--- layout: fc_discuss_archives title: Message 105 from Frama-C-discuss on October 2008 ---
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