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!

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