search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Local function #9

Open vprevosto opened 7 years ago

vprevosto commented 7 years ago

Would it be possible to define logic symbols local to a function contracts (in which the formals of the function would be in scope, and that could be used anywhere in the contract)?

davidcok commented 6 years ago

The syntax at least might be easy:

\let f(integer i) = i + 1; f(i+j) + 1 == f(i) + f(j)

or even

\let f(integer i) ={ ... return ...; }; ...

vprevosto commented 6 years ago

I'm not sure I'm following you, but the description of the issue would probably be clearer with an example, so here it is. Do you mean something like that?

/*@ \let f(integer k) = k + 1;
requires f(i) == j;
ensures f(\result) == i + j;
int c_func(int i, int j)

For me, the potential semantical issue is when the local function accesses memory state, so that its evaluation differ between requires and ensures, as in


/*@ \let deref{L} = *p;
requires \valid(p) && deref(p) == 0;
ensures deref(p) == 42;
*/
void f(int *p);