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] Problem with loop invariant

  • Subject: [Frama-c-discuss] Problem with loop invariant
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Fri, 09 Jul 2010 14:50:36 +0200
  • In-reply-to: <4C36E4B8.2060603@inria.fr>
  • References: <1276795121.1681.16.camel@iti27> <4C1F2AF5.3000604@inria.fr> <1277298042.2073.36.camel@iti27> <14634911.194632.1277726661282.JavaMail.www@wwinf8302> <1277728372.1482.21.camel@iti27> <4C36E4B8.2060603@inria.fr>
The code is from a student and I believe that the postcondition of some
of the called functions does not suffice to prove the loop invariant.

In this code, the loop invariant is indicated with a green check mark
whereas the assertion is marked by red scissors. If I understand you
right, all that this means is that assertion ==> loop invariant was
proved. I previously believed that the green mark means that the loop
invariant is valid.

Since this is easily misleading, I suggest to change the semantics of
check marks:

Let S1;...;Sn be a function with precondition P_pre and let P be a
proposition on Sm (1 <= m <= n).

- a green check mark on P means that {P_pre}S1;...;Sm{P} is valid.
- a yellow check mark on P means that there is a proposition Q and a k <
m such that {Q}Sk;...;Sm{P} is valid.

The second case corresponds to the meaning of a green check mark as of
now.

This way, the user can distinguish between propositions that are valid
and those that are merely an implication of some unproven proposition
within that function. This helps in debugging.

-- 
Regards,
Boris