1
Vote

spurious warning on cyclic pure function with termination measure

description

If a pure function has a _(decreases) clause, there is no reason to give a warning for a cycle in pure function calls. (Indeed, we should only give a warning if there is a cycle of functions, none of which has a measure.) We could leave the warning in when termination checking is turned off via a switch.

comments

erniecohen wrote May 26, 2012 at 11:46 PM

Note that this also means that if a recursive function has termination measure but no body, the postcondition can be of the form _(ensures \result == e) for any e, but we just verify it as iff the body of the function is { returns e; }.

erniecohen wrote May 26, 2012 at 11:53 PM

I think we should even go further, and just depricate pure functions without bodies and termination measures. The rules for functions without bodies are just crazy hacks, and run completely contrary to our constructive philosophy. Does anybody object?

fdupress wrote May 27, 2012 at 10:03 AM

I like (and make use of) the abstraction possibilities provided by _(abstract ...). One needs to make sure that all functions do get a verified body eventually (so we remain constructive and sound), but we don't need to carry that body around all the time, and we should indeed be able to switch one body for another (this is actually great for refinement proofs, which you wanted more support for).

If you simply meant real (non-ghost) functions that are declared as _(pure ...), then I don't object.

erniecohen wrote May 27, 2012 at 2:53 PM

I didn't mean just non-ghost functions. I meant that we should stop trying to prove the existence of a function satisfying a given postcondition and just force the user to provide an explicit witness. I'm fine with leaving out the body and getting a warning that a body is needed, or even _(assume_body) or something. I'd even be okay with changing the macro _(returns e) to provide the default body "return e".

None of this stops you from changing out one body for another.

MichalMoskal wrote Jul 31, 2012 at 11:04 PM

Yes, _(pure) functions should be deprecated, or rather they should behave as _(abstract) function (which in turn should be deprecated).

erniecohen wrote Jan 5 at 8:05 PM

(Don't know why I forgot to reply to Michal's comment before.)

I don't think we can deprecate _(pure) functions, just _(pure) functions without bodies and (possibly implicit) termination measures.

Sign in to add a comment or to set email notifications