Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] How to make sure the loop invariant or loop assign is complete/sufficient for proving those post-conditions?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Fri, 15 Nov 2013 15:29:41 +0100
  • In-reply-to: <CAA1cxujk9rW0o53bQu=n3UWMtyqBq8c=ZAfx4D0hE+qQRRkKpQ@mail.gmail.com>
  • References: <CAA1cxujk9rW0o53bQu=n3UWMtyqBq8c=ZAfx4D0hE+qQRRkKpQ@mail.gmail.com>
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