--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on February 2015 ---
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