diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-02 18:17:31 -0800 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-02 18:17:31 -0800 |
commit | f2d02cf07f597ebda226a0e55d3d2e5faf9c85b9 (patch) | |
tree | 63095fdee6b1d0d5b18c796b6d2c95350769cb2b /Test/dafny0 | |
parent | dd0e7dbe258dbf9dd090d94a621fb82c186a3c4c (diff) |
Dafny: tests for skeletons
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Skeletons.dfy | 63 |
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 + ...; + } +} |