--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on March 2019 ---
Hello Virgile, Sorry for the more-than-very-late-reply. ;-) A few comments below. Le 30/01/2019 à 19:40, Virgile Prevosto a écrit : > Indeed, being forced by the formal spec to expose more of the > implementation can't be seen as moving in the good direction ð. I > tend to think that what is missing there in ACSL is the possibility to > have two contracts for the same function, a "private" one (with full > access to static (global) variable), and a "public" one, which would > be more abstract. Of course, we would also need some way to express > the bindings between both contracts. I agree that such kind of abstraction might be needed in some cases but is it really needed in that very simple case? Does it help to *easily* prove wanted properties? > Going back to the counter example, something like that might fit the > bill in terms of "public" contract > > /*@ ghost int* __internal_region; */ > > /*@ axiomatic Internal { >  logic integer counter{L} reads *__internal_region; >  axiom valid_region: \valid(__internal_region); > } > */ > > /*@ >  requires counter < 1000; //cheap way to get rid of overflows >  assigns *__internal_region; >  ensures counter == \at(counter, Pre) + 1; >  ensures \result == counter; > */ > int f(void); > > > In order to show that the following definition respects the contract, > we'd then need to have ACSL extensions for defining the link between > the counter logic variable and c static variable (i.e. generating the > 'binding' assert, and setting their status to Valid, possibly after > generating additional lemmas/verification conditions if the > relationship between the internal state of the function and its logic > model is not as simple as is the case here)  > > int f() { > static int c = 0; > //@ assert binding: __internal_region == &c; > //@ assert binding: c == counter; > c++; > //@ assert binding: c == counter; > return c; > } > You might need to add some syntactic sugar but at least in the above form I find your proposal overly complicated (e.g. use of __internal_region). Best regards, david