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?

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