--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Preservation of base loop invariant not verified



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.