--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on January 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] scoping of 'axiomatic' declarations



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 @*/