--- layout: fc_discuss_archives title: Message 106 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!



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.
> ...