Lexicalscope

software engineering

Posted on July 31, 2014 by Tim Wood, Modified on October 8, 2014

The general method in Dafny for proving something of the form forall x :: P(x) ==> Q(x) is:

lemma X()
    ensures forall x :: P(x) ==> Q(x);
{
    forall x | P(x)
        ensures Q(x);
    {
       // prove Q(x)
    }
}