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



Ah, much clearer. Thanks!

-- Khairul


On Tue, Jan 27, 2015 at 11:37 PM, Claude Marche <Claude.Marche at inria.fr>
wrote:

>
>
> 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                    |
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150128/d508cd04/attachment.html>