--- layout: fc_discuss_archives title: Message 107 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Partial correctness explained to children!



Hi,

I do not mean to alter in any way what was decided for ACSL. I am just
saying that the Jessie plugin default is to generate termination VC only for
those loops annotated with variants. I recall that the Jessie plugin is not
ACSL!

Yannick


On Thu, Oct 23, 2008 at 2:55 PM, Pascal Cuoq <Pascal.Cuoq@cea.fr> wrote:

>
> On Oct 23, 2008, at 2:28 PM, Yannick Moy wrote:
>
>>  It is still to be decided whether we define an option to force
>> termination checking, or if this should be the default, with an option to
>> switch back to the current behavior.
>>
>
> Actually, I think that it has been decided that a clause "terminates p;"
> can be part of a function contract in ACSL, and that a function is
> acceptable
> with respect to such a contract as long as it terminates every time
> p is true in its pre-state (keeping in mind that the pre-condition is
> supposed to hold in the pre-state too, so that the function does not
> have to terminate if p holds but the pre-condition doesn't).
>
> Partial correctness results can be expressed by adding
> a "terminates false;" clause to the contract every function in the program.
> It would be bad style if the meaning of contracts
> changed according to command-line options.
>
> Further explanations and examples are provided in section 2.5
> of version 1.3 of the ACSL document, which reflects what was
> agreed on by the ACSL committee as far as I remember.
>
> Pascal
>
>


-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081023/4730322c/attachment.htm