--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on January 2015 ---
In fact, this does not seem to be the reason. It is not proved just because the trivial loop invariant below is missing loop invariant j >= 1; with this additional info, the preservation of the loop invariant loop invariant j == 1 ==> i == \at(i, LoopEntry) + loop(0); is a triviality, since j == 1 is false after any iteration of the loop. Anyway, I don't see why your loop invariant is splitted into two parts: this should work : /*@ loop invariant j >= 1; loop invariant i == \at(i, LoopEntry) + loop(j - 1); loop invariant j >= 8 ==> is_hello_printed == 1; loop assigns i, j, is_hello_printed; loop variant 10 - j ; */ Hope this helps, - Claude Le 26/01/2015 10:05, Lo?c Correnson a ?crit : > Your property P is not provable *by induction* ; it means that P(j+1) is not a logic consequence of P(j). > (read in the WP manual about the proof obligations generated for loop invariants). > Actually, there is nothing in your loop invariants about the value of (i) at any loop turn? > L. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |