asserting things about methods?

Jun 17, 2016 at 7:11 PM
Edited Jun 17, 2016 at 7:23 PM
I'd like to be able assert things about the results of Dafny methods
that have side-effects, for example that two methods return the same
thing (see predicate p() in the simple example below). When I try to
do this, Dafny complains that expressions can't invoke methods. I
imagine I could work around this by using only the functional sub-set
of Dafny, but that would be a pain. Is there a more straightforward
way to assert things about methods?

class C {
var x : int;

ghost method m1(y : int) returns (z : int)
  modifies this;
{
  x := 0;
  return x;
}

ghost method m2(y : int) returns (z : int)
  modifies this;
{
  x := 0;
  return x;
}

predicate p()
{
  forall w :: m1(w) == m2(w)
}
}
Coordinator
Jun 18, 2016 at 9:30 PM
The only way to do this is to add to both m1 and m2 some postcondition that is strong enough for you to be able to conclude what you want.

It sounds a little like you're trying to say that one method is a refinement of the other. If so, maybe Dafny's features for program refinement will have what you need, see "Programming Language Features for Refinement", Koenig and Leino, EPTCS, 2016, http://research.microsoft.com/en-us/um/people/leino/papers/krml248.pdf).

Rustan