Non-determinism in Dafny

Coordinator
Jul 10, 2014 at 11:40 PM
A question someone just asked me is: "How do I model non-determinism in Dafny?"
Coordinator
Jul 10, 2014 at 11:42 PM
There are many ways to get non-determinism in Dafny. For example, you can assign an arbitrary value to a variable:
x := *;
Or, when you declare a variable (and don’t assign it a specific value), Dafny will give it an arbitrary value. For example:
var n: nat;
var x;
In this example, the type of n is specified whereas the type of x will be inferred from the rest of the program.

You can also use an assign-such-that statement. For example:
x :| 20 <= x < 100;
sets x to a value such that x satisfies 20 <= x < 100.

Yet another way is to use a function or method that returns a value, but where the function or method has no defining body. In that case, Dafny will treat the value returned as being anything (more precisely, as anything that satisfies the given postcondition, if any).
method AnyValue(x: int) returns (r: int)
  ensures x < r;  // the return value is larger than the argument

method Client()
{
  var y := AnyValue(15);  // this will set y to any arbitrary value larger than 15
}
In simple cases, perhaps you just want the non-determinism to influence control flow. You can then write:
if * {
  // do something here
} else {
  // do something else here
}
Or, a pretty way to do this, perhaps especially when you have more than 2 alternatives, is to use an "if fi" construction:
if {
  case true =>  // do something here
  case true =>  // do something here
  case x < 10 =>  // do something here
  case true =>  // do something here
}
In this example, one of four somethings will take place, but the third something will take place only if x is less than 10.

Rustan