diff options
author | 2013-03-05 17:01:25 -0800 | |
---|---|---|
committer | 2013-03-05 17:01:25 -0800 | |
commit | 9f7c11c0a12a9b802f23d613abeee91a2fb47743 (patch) | |
tree | ff0c5ffd982094c5d03828f1332be03a4d66b4ea /Test/dafny0/RefinementErrors.dfy | |
parent | c819fabbb8da669952cb7e2e5937c73ff6dcfabe (diff) |
Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories.
Diffstat (limited to 'Test/dafny0/RefinementErrors.dfy')
-rw-r--r-- | Test/dafny0/RefinementErrors.dfy | 58 |
1 files changed, 0 insertions, 58 deletions
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy deleted file mode 100644 index df6f1a71..00000000 --- a/Test/dafny0/RefinementErrors.dfy +++ /dev/null @@ -1,58 +0,0 @@ -module A { - class C { - method M(y: int) returns (x: int) - { - x := 6; - } - - var abc: bool; - var xyz: bool; - - function method F<A,B,C>(x: int, y: A, z: set<C>, b: bool): B - - function G(): int // uninterpreted for now - function H(): int // uninterpreted for now - - method BodyLess(y: bool, k: seq<set<object>>) returns (x: int) - method FullBodied(x: int) returns (y: bool, k: seq<set<object>>) - { - } - } -} - -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 - - predicate abc // error: cannot replace a field with a predicate - var xyz: bool; // error: ...or even with another field - - function F // error: cannot replace a "function method" with a "function" - <C,A,B> // error: different list of type parameters - (x: int, y: A, z: seq<C>, // error: different type of parameter z - k: bool) // error: different parameter name - : B - - function G(): int - { 12 } // allowed to add a body - - method BodyLess(y: bool, k: seq<set<object>>) returns (x: int) - { // yes, can give it a body - } - method FullBodied(x: int) returns (y: bool, k: seq<set<object>>) - { - } - } -} - -module BB refines B { - class C { - function method G(): int // error: allowed to make a function into a function method - function method H(): int // ...unless this is where the function body is given - { 10 } - } -} |