--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Requirements as hypothesis for assumes ?



Dear,

When proving a function including a function call, such as the following g function:

/*@ requires Rf;
   @ behavior a:
   @   assumes Af;
   @   ensures Ef;
*/
int f(int x){....}

/*@ requires Rg;
   @ ensures Eg;
*/
int g(int x){
   <instructions1>
   y=f(z);
   <instructions2>
}


Here is the proof obligation that we need to proof to establish the correctness 
of g:

   Rg => [<instructions1>;y=f(z);<instructions2>]Eg


In Jessie, it seems to be rewrites into a formula like:

   Rg => [<instructions1>](Rf & (Af & Ef => [<instructions2>]Eg))


And then split into two PO separating precondition and postcondition:

   1) Rg => [<instructions1>]Rf
   2) Rg => [<instructions1>](Af & Ef => [<instructions2>]Eg)



However, it could be appreciate to have [<instructions1>]Rf as hypothesis of 
(2). Indeed, (1) can be an interesting hypothesis in order to establish if the 
assumes clause Af holds or not.

An extreme example is the one where (Af = Rf). In a such case, we need to 
establish (1) during the proof of (2).


Do you think than adding the requirement clause as hypothesis as in the 
following have any sense ?

1) Rg => [<instructions1>]Rf
2) Rg && [<instructions1>]Rf => [<instructions1>](Af & Ef =>[<instructions2>]Eg)

Thanks,
Nicolas.
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: nicolas_stouls.vcf
Type: text/x-vcard
Taille: 445 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090804/d0cd1a7e/attachment.vcf