Dafny Proof by Contradiction

The general method in Dafny for proving something by contradiction is:

lemma X()
    ensures Q(x)
{
    if !Q(x)
    {
       // derive contradiction
       assert false;
    }
}

Leave a Reply

Your email address will not be published. Required fields are marked *