Dafny: tests for skeletons

1 files changed, 63 insertions, 0 deletions

diff --git a/Test/dafny0/Skeletons.dfy b/Test/dafny0/Skeletons.dfy
new file mode 100644
index 00000000..e9fef946
--- /dev/null
+++ b/Test/dafny0/Skeletons.dfy
@@ -0,0 +1,63 @@
+module A {
+  method M(p: int) returns (y: int)
+    requires p <= 30;
+  {
+    assume p < 100;
+    var x;
+    assume x == p + 20;
+    x := x + 1;
+    while (*)
+      invariant x <= 120;
+      decreases 120 - x;
+    {
+      if (x == 120) { break; }
+      x := x + 1;
+    }
+    y := x;
+  }
+}
+
+module B refines A {
+  method M ...
+  {
+    assert p < 50;
+    assert ...;
+    var x := p + 20;
+    assert ...;
+    var k := x + 1;
+    ...;
+    while ...
+      invariant k == x;
+    {
+      k := k + 1;
+    }
+    assert k == x || k == x + 1;  // there are two exits from the loop
+  }
+}
+
+
+module C0 refines B {
+  method M ...
+    ensures y == 120;  // error: this holds only if the loop does not end early
+  {
+  }
+}
+
+module C1 refines B {
+  method M ...
+    ensures y <= 120;
+  {
+  }
+}
+
+module C2 refines B {
+  method M ...
+    ensures y == 120;
+  {
+    ...;
+    while (true)
+      ...
+    assert k == x + 1;  // only one loop exit remains
+    ...;
+  }
+}