--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on January 2010 ---
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