--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: assigns needed to prove function contract?



Hello Lo?c,

2013/9/9 Lo?c Correnson <loic.correnson at cea.fr>:
> However, modifying [v] at each loop that your loop invariant are to weak : they do not relate a[..] values with the v at the Pre state of the function, but with the current value of v at each loop iteration.
>
> But, the value of v occurring in the post state is the one of the formal parameter, aka \at(v,Pre).
> The same remark applies to variables a and n.
>
> You can add the following invariants :
>
> loop invariant n == \at(n,Pre);
> loop invariant a == \at(a,Pre);
> loop invariant v == \at(v,Pre);
>
> to make your post-conditions provable, even with a missing loop assigns clause.

Thank you for the clear explanation.

> Jessie makes this kind of analysis and the (non-distributed) plugin GenAssigns infer missing assigns clauses like those.

Maybe it would be interesting for WP to gain such capabilities, at
least from a user point of view. ;-) Or maybe you have some use case
in mind that need some manual writing of loop assigns.

Sincerely yours,
david