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] scoping of 'axiomatic' declarations

  • Subject: [Frama-c-discuss] scoping of 'axiomatic' declarations
  • From: dcok at grammatech.com (David R. Cok)
  • Date: Sat, 16 Jan 2016 20:06:39 -0500
The acsl 1.9 document is unclear about the scoping of names declared in 
an axiomatic declaration.

In the given example, are the declarations all essentially global and 
the name IntList just for convenience
or is there some sort of scoping happening, like IntList::int_list or 
IntList::append_cons?

- David


1 /*@ axiomatic IntList {
2 @ type int_list;
3 @ logic int_list nil;
4 @ logic int_list cons(integer n,int_list l);
5 @ logic int_list append(int_list l1,int_list l2);
6 @ axiom append_nil:
7 @ \forall int_list l; append(nil,l) == l;
8 @ axiom append_cons:
9 @ \forall integer n, int_list l1,l2;
10 @ append(cons(n,l1),l2) == cons(n,append(l1,l2));
11 @ }
12 @*/