Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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