--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on March 2009 ---
Hello Virgile, On Wed, Mar 18, 2009 at 17:54, Virgile Prevosto <virgile.prevosto at cea.fr> wrote: > if the code of the reduced example is exactly like above, the assertion > is not proved, since the lack of '@' means that it is not seen as an > ACSL annotation. Ohh! I'm ashamed. :-( > If you put back the '@', there is another issue: the > assertion is false. Namely, if you call f with n == 0, the loop is not > entered, and total is still 0 at this point. Ah yes. I realized that in my larger example that's why I wrote the following pre-condition. > Now the larger example has a stronger pre-condition (0< > num_candidates). So why does alt-ergo still fail on the assertion? > Well, remember that the only thing that jessie 'knows' after a loop is > its invariant, I realized that more or less by trial and error. Is this written somewhere in Jessie documentation? I have probably read it but overlooked it. By the way, I have seen that some "global" knowledge is also kept (assertions about global variables? function pre-condition?). Is this correct? Is this described somewhere? > and here the loop invariant is too weak: it gives an > upper bound for total, but no lower bound. A possibility (short of the > ACSL construction \sum which is currently unsupported by jessie) would > be to add the following invariant: > > loop invariant \forall integer j; 0<=j<i ==> total >= counters[j]; Thank you. I'll try that. I have a side question: I usually write \forall assertions with an int: "\forall int i; [...]". You write your assertion with "integer", "\forall integer i; [...]". Is there any difference? Any reason to prefer one over the other? Sincerely yours, david