--- layout: fc_discuss_archives title: Message 111 from Frama-C-discuss on November 2013 ---
Dear David, Many thanks for your kindness help. > > The loop invariant should provide enough information at each loop step > to prove a property when exiting the loop. > > Roughly speaking, the loop invariant: > * Should be true at loop entry, at each loop step and at loop exit > (see Frama-C manual for precision definition of those); > > * Should progressively built the property which is tied to the code > inside the loop. Usually you have a property true until step i of a > loop. You can assume that the property is true at step i to prove > property at step i+1. > Thanks. Very clear explanation. At the same time, I also read related blogs about formal verification (including your blog). Yes, Indeed, for verifying a function that has loop, we need to provide concrete loop invariants. Other verification tools also need these informations. (deductive verification) I am not very sure is there any other verification tools that using other techniques other than deductive verification for loops. > When you are able to prove your post-condition. ;-) > ;-(, this is really boring... But seems we have no other solution right now. > > loop invariant is the logical property that your loop builds. Loop assign > is the set of location assigned within the loop. The two are linked, > loop assign can help prove properties in the loop invariant > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-September/thread.html#3830 > for a detailed example). Jessie and WP can have different behaviours. Actually, I try the function you provide many times. for example, I change this two lines "loop assigns i; loop variant n - i;" into: "loop invariant n; loop variant i;" I thought they are the same. But some properties can't be proved. This makes me really confused. I don't know any different between these two. Thanks again. -david