--- layout: fc_discuss_archives title: Message 108 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to make sure the loop invariant or loop assign is complete/sufficient for proving those post-conditions?



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