--- layout: fc_discuss_archives title: Message 108 from Frama-C-discuss on November 2013 ---
Hello David, 2013/11/15 David Yang <abiao.yang at gmail.com>: > 1. How many or on what extent should the loop invariant provided? 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. > 2. How can we make sure that the provided loop invariant is enough for > the verification? When you are able to prove your post-condition. ;-) You can put "assert" at various points in your code (inside the loop, at loop entry or exit, ...) to check that what you think should be proved is indeed proved. You can also compile and test your loop invariant with e-acsl plug-in (very effective!). > 3. What is the main different between loop invariant and loop assign? > since sometimes only provide loop assign is enough for proving some > post-conditions. For precise definition, see Frama-C manual. Roughly speaking, 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 (for example see this thread 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. Best regards, david