Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] polymorphic logic types and the use of type parameters?
- Subject: [Frama-c-discuss] polymorphic logic types and the use of type parameters?
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Thu, 12 Feb 2015 11:49:03 +0100
- In-reply-to: <87bnl1e60j.wl-MarkoSchuetz@web.de>
- References: <87bnl1e60j.wl-MarkoSchuetz@web.de>
Hello Marko, 2015-02-10 23:49 GMT+01:00 Marko Sch?tz Schmuck <MarkoSchuetz at web.de>: > Dear All, > > for a list parameterized on the element type, I'd like to write: > > /*@ axiomatic List { > @ type list<A>; > @ logic list<A> nil; > @ logic list<A> cons(A x, list<A> xs); > @ ... > @*/ > > Frama-C Neon signals an error in line 4 > > user error: unexpected token 'A' > > Is this due to the experimental nature of support for parameterized > types? Can I fix this easily or will I have to wait for a future > version of Frama-C? In theory, you should make the <A> parameter explicit in the declaration of the functions themselves: /*@ axiomatic List { @ type list<A>; @ logic list<A> nil<A>; @ logic list<A> cons<A>(A x, list<A> xs); @ } @*/ However, Frama-C does not seem to accept nil<A>: polymorphic.c:3:[kernel] user error: some type variable appears only in the return type. All type variables need to occur also in the parameters types. in annotation. I'm not exactly sure I remember why this restriction has been put in place. Support for polymorphic types is indeed very experimental, and I'm afraid Sodium won't propose something much better. That said, for lists, you can declare it as a sum type that way: /*@ type list<A> = Nil | Cons(A,list<A>); */ the match construction is not implemented yet, but you can still define functions or predicates over lists axiomatically or inductively. Best regards, -- E tutto per oggi, a la prossima volta Virgile
- References:
- [Frama-c-discuss] polymorphic logic types and the use of type parameters?
- From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
- [Frama-c-discuss] polymorphic logic types and the use of type parameters?
- Prev by Date: [Frama-c-discuss] Problem with strlen
- Next by Date: [Frama-c-discuss] several WP questions
- Previous by thread: [Frama-c-discuss] polymorphic logic types and the use of type parameters?
- Next by thread: [Frama-c-discuss] several WP questions
- Index(es):