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

[Frama-c-discuss] Question regarding frama-c/jessie



Hello,

We would like to prove properties on the set of all before/after states
for a given operation. For instance, suppose I have a C operation with
the following specification.
/*@ requires x >= 0;
   @ ensures \result == x + 1;
*/
int increment(int x) {
    return x + 1;
}

I would like to prove a property like:

/*@lemma (\forall int x, int y; (x >= 0  &&  y >= 0            ----or
rather some shorthand to satisfy the requires of operation "increment"
                                               && y > x)  
                                                       ==>
                                                         
Semantics_Of("increment")(y) >
Semantics_Of("increment")(x))                      ---- i.e. operation
increment implements a monotonic function
*/


Could anyone tell me:
 * whether such properties are expressible in ACSL
 * is it supported by Frama-C and jessie
 * if not, what would be a good way to get around this limitation
 * if not, whether such extensions to ACSL are planned
 * whether there are significant issues blocking this kind of
expressivity in ACSL

Thank you
Regards
Damien