Does Dafny support "proof by construction"?

Question

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?

Answer 1

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.