Function Lemma Keyword

Nov 11, 2014 at 12:14 PM
Hi,

I found myself thinking it would be nice to have a function lemma keyword. Something like this:
function lemma MyLemma(x:int) 
   requires P(x);
   ensures Q(x);
{
  E
}
which is equivalent to
predicate MyLemma(x:int)
   requires P(x);
   ensures Q(x);
   ensures MyLemma(x);
{
   E
}
Cheers,

Tim
Coordinator
Nov 12, 2014 at 10:07 PM
Would the purpose of using it be to get the implication P(x) ==> Q(x) somewhere in the program?

How would you use it? Can you not just an ordinary lemma instead? Note that
SomeLemma(x); E
is an expression in Dafny. Semantically, it is the same as E, but the lemma is used when verifying the well-formedness of E.

Rustan
Nov 13, 2014 at 1:56 PM
Ahh, OK. Now I think that perhaps I am confused and having a syntax related problem.

I did not know how to write SomeLemma(x); E as an invariant, but I now I think it should perhaps be written with brackets (SomeLemma(x); E)