CODEWITHSUNDEEP
proofdafny
Jason Orendorff
Jason Orendorff

Reputation: 45086

Does Dafny support "proof by construction"?

Suppose I have a method that computes something:

method Difference(a: nat, b: nat) returns (c: nat)
  ensures a + c == b || b + c == a
{
  ...
}

Never mind the implementation for now. If I can implement this method in Dafny, that means that for all possible arguments a and b, there must be some return value c that fulfills the postcondition.

In other words, the body of the method is a constructive proof that:

forall a: nat, b: nat :: exists c: nat ::
  a + c == b || b + c == a

But Dafny is not convinced:

method Difference(a: nat, b: nat) returns (c: nat)
  ensures a + c == b || b + c == a
{
  c := if a > b then a - b else b - a;
}

method Main() {
  assert forall a: nat, b: nat :: exists c: nat ::  // error: assertion violation :(
    a + c == b || b + c == a;
}

Is there a way to use this kind of reasoning in Dafny?

Upvotes: 1

Views: 245

Answers (2)

James Wilcox
James Wilcox

Reputation: 5663

Valéry's answer is a good trick for cases where existence is proved by a lemma. You can also extend the trick to "hint inside a forall" using Dafny's forall statement, like this

forall a: nat, b: nat
    ensures exists c: nat :: difference_property(a, b, c)
{
    var c := difference(a, b);
    assert difference_property(a, b, c);
}

which proves the forall expression 

forall a: nat, b: nat :: 
    exists c: nat :: 
        difference_property(a, b, c)

For Jason's other question about using proper methods in proofs, Dafny does not support this. Indeed, I think it makes sense that it is not supported, since methods can have effects on the heap, for example. Thus, the construction of some witness may in principle depend on allocating state or even modifying existing state. Internalizing that effect into the logic is fishy and would change Dafny's nature.

Upvotes: 1

Valéry
Valéry

Reputation: 4704

This does the trick: wrap the property in a predicate, and prove the exists in a lemma, so that you can hint the verifier with an assert.

Maybe there is some way to hint inside a forall as well.

predicate difference_property(a: nat, b: nat, c: nat)
{
    a + c == b || b + c == a
}

function difference(a: nat, b: nat): nat
{
    if a > b then a - b else b - a
}

lemma main(a: nat, b: nat)
    ensures exists c: nat :: difference_property(a, b, c)
{
    var c := difference(a, b);
    assert difference_property(a, b, c);
}

Upvotes: 2

Related Questions