--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on May 2009 ---
>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