--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2009 ---
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