--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on January 2016 ---
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 @*/