--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2010 ---
Hollas Boris (CR/AEY1) wrote: > > However, I see a problem with a postcondition \true: Assume you have statements S; T in the code where S is a call of an unannotated function and T is some statement. Further, assume the verifier has shown {P} T {Q}, where P = wp(T,Q) is the weakest precondition of T wrt Q. Then, the verifier has to show that true -> P is valid, which means it has to show that P is valid. The problem I see is that the verifier will fail here. > > Maybe the verifier works differently? > Your remark would be true if the default assigns was "everything", but as said in previous mails it is not the case. If f() assigns \nothing, then you just need to prove P before the call to f(). Generally speaking, to prove that an assertion P is true after a method call f(...), what you need to prove is as follows. let me write S |= p to mean "program p runs correctly in memory state S". Thus to prove S |= f(...) {P}, you need to prove 1) S |= Pre(f) 2) for any memory state S' such that assigns(S,S',Locs(f)) and S' |= Post(f), S' |= P. here Locs(f) denotes the assigns clause for f, and assigns(S,S',Locs(f)) means "any memory location not in Locs(f) are the same in S and S'" Turning this into a rule for WP calculus needs to make precise the memory model. But if we assume a simple memory model represented by a variable Heap (thus *p is select(Heap,p), *p = v is Heap := store(Heap,p,v)) then you can say WP(f(),P)(H) = Pre(f) /\ forall H', (assigns(H,H',Locs(f)) && Post(f)(H')) ==> P(H') If Locs(f) is the empty set ("assigns \nothing"), then assigns(H,H',Locs(f)) reduces to H=H', and the whole reduces to WP(f(),P)(H) = Pre(f) /\ (Post(f)(H) ==> P(H)) If Post(f) is true, it reduces to WP(f(),P)(H) = Pre(f) /\ P(H) hence you have to prove both Pre(f) and P in the pre-state. Does it helps ? I'm not sure it was your question... - 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 |