Cannot prove in Dafny that f(a,b)=f(b,a)

Question

I m trying to prove in Dafny that a function is symmetric: i.e., f(a,b)=f(b,a). I specify this Dafny by doing ensures f(a,b) == f(b,a). However, it is not able to verify; but what I do not understand is that I get the following message: cannot prove termination; try supplying a decreases clause.

Since explaining my function f would be too verbose, I simply show the following dummy function:

function method dummy(a:real, b:real):real
   ensures dummy(a,b) == dummy(b,a)
   {
       a*b
   }

For which I receive the same message.

What am I doing wrong?

Answer 1

Functions are opaque within their own ensures clause, to avoid infinite recursion. For example, Dafny rejects this:

function method dummy(x: int): int
  ensures dummy(0) == 4
{
  4
}

Instead, you should use a lemma:

function method dummy(a:real, b:real): real {
  a*b
}

lemma DummySymmetric(a:real, b:real)
  ensures dummy(a, b) == dummy(b, a)
{}

If you really want to get the symmetry for free without having to call a lemma, you can wrap dummy into another function:

function method dummy(a:real, b:real): real {
  a*b
}

function method dummyWithLemma(a:real, b:real): (r: real)
  ensures r == dummy(b, a)
  // ensures dummyWithLemma(a, b) == dummy(b, a) // Also OK
{
  dummy(a, b)
}