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!

Thank you, Yannick and Pascal, for your answers and hints.

But ... would it be possible to keep that idea of a command-line option 
that will stress the end-users to specify mandatory "terminates ..." 
clauses either for functions containing loops, or for recursive 
functions, or for backward goto/label in functions (I promise there is 
no backward-goto in my code! but ... who knows in the world!!!).

Best regards,
Dillon

Pascal Cuoq a ?crit :
>
> 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.
> ...
>
> 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.
> ...