Test/dafny4/Juggernaut.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

method Jug()
{
  var x, y, z;
  while x > 0 && y > 0 && z > 0
    decreases x < y, z
  {
    if y > x {
      y := z;
      x := *;
      z := x - 1;
    } else {
      z := z - 1;
      x := *;
      y := x - 1;
    }
  }
}