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



>     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
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091210/8db4e7db/attachment.htm