1 files changed, 159 insertions, 0 deletions
diff --git a/Test/dafny0/BindingGuards.dfy b/Test/dafny0/BindingGuards.dfy
new file mode 100644
index 00000000..0706fc5b
--- /dev/null
+++ b/Test/dafny0/BindingGuards.dfy
@@ -0,0 +1,159 @@
+// RUN: %dafny /dprint:- /env:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(n: int)
+{
+  n % 2 == 0
+}
+
+predicate R(r: real)
+{
+  0.0 <= r
+}
+
+method M0()
+{
+  if x :| P(x) {
+    var y := x + 3;
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+  }
+}
+
+method M2()
+{
+  var x := true;
+  if x, y :| P(x) && R(y) {  // this declares a new 'x'
+    var z := x + 12;
+  }
+  x := x && false;
+}
+
+method M3()
+{
+  var x := true;
+  if x: int, y :| P(x) && R(y) {
+    var z := x + y.Trunc;
+    var w := real(x) + y;
+  }
+}
+
+method M4()
+{
+  if x, y: real :| P(x) && R(y) {
+  }
+}
+
+method M5()
+{
+  if x: int, y: real :| P(x) && R(y) {
+  }
+}
+
+method M6()
+{
+  if x {:myattribute x, "hello"} :| P(x) {
+  }
+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+  }
+  if x: int {:myattribute x, "chello"} :| P(x) {
+  }
+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+  }
+}
+
+ghost method M7() returns (z: real, w: real)
+  ensures -2.0 <= z
+  ensures z == w  // error: does not hold
+{
+  var k;
+  if x :| P(x) {
+    k, z := 4, 18.0;
+  } else if * {
+    z := z + -z;
+  } else if y :| R(y) {
+    z := y;
+  } else if y :| P(y) {
+    k := y;
+  } else {
+    z :| R(z);
+  }
+  if P(k) {
+    z := 18.0;
+  }
+}
+
+ghost method M8(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  var t := -1;
+  var u;
+  if y :| m <= y < n && P(y) {
+    u := y;
+    if * {
+      t := n - y;
+    } else if * {
+      t := y - m;
+    } else if P(y) {
+      t := 8;
+    } else {
+      t := -100;  // will never happen
+    }
+  }
+  if t < 0 && m < n {
+    assert P(m) && !P(m);
+    assert false;
+  }
+  assert t < 0 ==> n <= m;
+}
+
+method P0(m: int, n: int)
+  requires m < n
+{
+  ghost var even, alsoEven := 4, 8;
+  if {
+    case x :| P(x) =>
+      even := x;
+    case x: int :| P(x) =>
+      even := x;
+    case x, y :| P(x) && R(y) =>
+      even, alsoEven := x, y.Trunc;  // this assigns to 'alsoEven' a possibly odd number
+    case x: int, y :| P(x) && R(y) =>
+      even := x;
+    case m < n =>  // just to be different
+    case x, y: real :| P(x) && R(y) =>
+      even := x;
+    case x: int, y: real :| P(x) && R(y) =>
+      even := x;
+  }
+  assert P(even);
+  assert P(alsoEven);  // error: may not hold
+}
+
+method P1(m: int, n: int)
+{
+  if {  // error: missing case
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P2(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  if {  // error: missing case
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P3(m: int, n: int)
+  requires m < n && forall y :: m <= y < n ==> P(y)
+{
+  assert P(m);  // lemma that proves that the following 'if' covers all possibilities
+  if {
+    case x :| m <= x < n && P(x) =>
+  }
+}