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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Mon, 01 Feb 2010 15:36:42 +0100
  • In-reply-to: <4B62E1D5.5010500@adelard.com>
  • References: <4B62E1D5.5010500@adelard.com>
Damien Karkinsky wrote:
> 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
>   

There is no direct support for that kind of property in ACSL. However, 
there are some tricks to acheive the same.
The idea is the define an additional function which will call the 
former. For example:

//@ requires x >=0 && y >= 0 && y > x;
void check_increment_monotonicity(int x, int y) {
    int res_x = increment(x);
    int res_y = increment(y);
    //@ assert res_y > res_y;
}

I hope you get the idea... But beware, if the property you want depends 
on the global state, it will not work.
Some methods based on this idea have been proposed, for example to prove 
properties of non-interference, e.g. private data can not be observable 
from public data.

The general idea is, as above, to execute two independent copies of the 
code, but you have also to have two different copies of the heap in some 
sense.

You could also look at the following paper which proposes methods to 
prove program equivalence using Frama-C:

@inproceedings{almeida09fmics,
 author = {Almeida, Jos\'{e} Bacelar and Barbosa, Manuel and Sousa 
Pinto, Jorge and Vieira, B\'{a}rbara},
 title = {Verifying Cryptographic Software Correctness with Respect to 
Reference Implementations},
 booktitle = {Proceedings of the 14th International Workshop on Formal 
Methods for Industrial Critical Systems (FMICS'09)},
 year = 2009,
 isbn = {978-3-642-04569-1},
 pages = {37--52},
 doi = {http://dx.doi.org/10.1007/978-3-642-04570-7_5},
 publisher = SV
 }

Hope this helps,

- Claude


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |