--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Loop invariants



>Sure if condition is (i < n) or anything that implies (i < n), but
>otherwise no. But if you are able to prove that the invariant holds,

Ok, this answers my question.

>then certainly you should be able to prove //@ assert i<n; either before

Yes, this should be possible. I wondered whether Jessie is able to deduce this on its own.

- Boris