--- layout: fc_discuss_archives title: Message 21 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




On 01/27/2015 01:14 PM, Khairul Azhar Kasmiran wrote:
> Aha! So the problem was because the solvers did not receive any
> information on the lower bound of j. Hmm, okay. Still unclear to me as
> to why it's needed, since the invariant doesn't state that j == 1 is
> false after any iteration of the loop.

Any loop iteration increments j by 1, no ? then if j >= 1 before the 
iteration, then j >= 2 after. And consequently j == 1 is false. Qed.

- Claude

-- 
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                    |