--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2010 ---
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