--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2012 ---
Hello David, 2012/5/9 David MENTRE <dmentre at linux-france.org>: > > Goal store_cisapb_post_1 cannot be proved. You probably meant "ensures > Equal{Post}(a, b, c, n);", i.e. equality on Post state. Equality in > Pre state is obviously invalid. With this modification this VC is > proved. > > For store_cisapb_loop_inv_2_preserved goal, I have used a slightly > different loop invariant: > """ > loop invariant \forall integer k; 0 <= k < i ==> c[k] == a[k] + b[k]; > """ > > For store_cisapb_assert_6_rte goal, I used the same assumption as you, > only limiting the assumption to 0 <= k < n. > For what it's worth, strictly speaking, it is not necessary to unfold the definition Equal in the loop invariant: I didn't succeed to have it discharged automatically, but you can convince Coq that it is true (I don't append the script here, especially given the fact that I'm using the development version of Frama-C, but if someone is interested, feel free to ask). My guess is that automated provers have trouble relating the Equal predicate of the previous loop step (given as hypothesis) and the Equal of the current step (the goal of the proof obligation), but this might require further investigation. Best regards, -- E tutto per oggi, a la prossima volta Virgile