Dijkstra-style IF---FI and DO---OD

May 3, 2014 at 10:54 AM
What's the best Dafny-up-to-date way of expressing Dijkstra-style

IF gd1 -> bd1 | gd2 -> bd2 FI
DO gd1 -> bd1 | gd2 -> bd2 OD

where the guards can overlap, causing a potential nondeterministic choice?


[ I'm aware of the nondeterministic constructs x:| and x:= *. ]
May 3, 2014 at 2:42 PM
Dafny supports these statements. The syntax is:
if {
  case gd1 => bd1;
  case gd2 => bd2;
while {
  case gd1 => bd1;
  case gd2 => bd2; 
If you need invariant, decreases, or modifies clauses for this loop, just place them before the open curly brace, as you would for the ordinary while statement.

By the way, another way to use nondeterminism in the language is in the guards of if and while statements, where you can write *. For example:
if * {
} else {
while * {
This loop may or may not ever terminate, so to achieve termination you'll need to have some other break or return statement in Body. (Or, you can mark the loop with decreases *;, which says that you're okay with the possibility that the loop does not terminate and, thus, that don't want termination checking.

Marked as answer by rustanleino on 5/3/2014 at 9:17 AM