--- layout: fc_discuss_archives title: Message 111 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?



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