Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Question regarding frama-c/jessie
  • From: dak at adelard.com (Damien Karkinsky)
  • Date: Fri, 29 Jan 2010 13:25:41 +0000
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