diff options
author | 2012-01-09 23:16:37 -0800 | |
---|---|---|
committer | 2012-01-09 23:16:37 -0800 | |
commit | 814a47c0b8d492f7dcfe9b815c74350b4893f4a6 (patch) | |
tree | da65f0d02489ff6934fcfd905b25307540df13ce /Test/dafny0/RefinementErrors.dfy | |
parent | 4dc9d5a6a2b2e1ae3513016b34341dbf0959da3c (diff) |
Dafny: added support for simple superposition refinements
Diffstat (limited to 'Test/dafny0/RefinementErrors.dfy')
-rw-r--r-- | Test/dafny0/RefinementErrors.dfy | 65 |
1 files changed, 13 insertions, 52 deletions
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy index de8694b3..b10c035e 100644 --- a/Test/dafny0/RefinementErrors.dfy +++ b/Test/dafny0/RefinementErrors.dfy @@ -1,57 +1,18 @@ -class A refines C { -} - -class B refines A { -} - -class C refines B { -} - - -class D { - refines M() - { - } -} - -class E { - var x: int; - - method M() - { - x := 0; - } -} - -class F { - replaces M by x == y; -} - -class G refines E { - var y: int; - replaces x by x == y; - - refines M() returns (i: int) - { +module A { + class C { + method M(y: int) returns (x: int) + { + x := 6; + } } } -class H refines E { - var x: int; - - method M() - { +module B refines A { + class C { + var k: int; + method M(y: int) returns (x: int) + requires 0 <= y; // error: cannot add a precondition + modifies this; // error: cannot add a modifies clause + ensures 0 <= x; // fine } } - -class J refines E { - var y: int; - replaces x by x == y; - - refines M() - { - y := 1; - } -} - - |