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

[Frama-c-discuss] Help with proving post-conditions



You're right, it should. Thanks for that.

I fixed that however still not proving the post-conditions, are my loop
invariants too weak/wrong?

 

From: frama-c-discuss-bounces at lists.gforge.inria.fr
[mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pascal
Cuoq
Sent: Thursday, December 10, 2009 3:40 PM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] Help with proving post-conditions

 

 

    ensures \forall integer j; strlen{Old}(s) <= j <= strlen(s) ==> s[j] ==
append[j];

This should be append[j-strlen{Old}(s)], should it not?

 

Pascal

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091210/807bdd03/attachment.htm