diff options
author | kyessenov <unknown> | 2010-07-03 06:43:54 +0000 |
---|---|---|
committer | kyessenov <unknown> | 2010-07-03 06:43:54 +0000 |
commit | c74aa37687000b2cdbc3ecae9b5a78d1dd8f6b51 (patch) | |
tree | e7af7c5c4a5eb4ee87a0f254526a92631cc61a55 /Test/dafny0/Refinement.dfy | |
parent | eea8a58628915f7b3f9efd891282543defd40489 (diff) |
Dafny: added assertions in the refinement obligation necessitating that the return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
Diffstat (limited to 'Test/dafny0/Refinement.dfy')
-rw-r--r-- | Test/dafny0/Refinement.dfy | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index 205f3b6c..c10d86f3 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -18,7 +18,7 @@ class A { method Test1(p: int) returns (i: int) { - assume true; + i := p; } method Test2() returns (o: object) @@ -51,7 +51,17 @@ class B refines A { // Carrol Morgan's calculator // 7/2/2010 Kuat +class Util { + static function method seqsum(x:seq<int>) : int + decreases x; + { + if (x == []) then 0 else x[0] + seqsum(x[1..]) + } +} + + class ACalc { + var util: Util; var vals: seq<int>; method reset() @@ -69,21 +79,17 @@ class ACalc { method mean() returns (m: int) requires |vals| > 0; { - m := seqsum(vals)/|vals|; - } - - static function method seqsum(x:seq<int>) : int - decreases x; - { - if (x == []) then 0 else x[0] + seqsum(x[1..]) + m := util.seqsum(vals)/|vals|; } } + class CCalc refines ACalc { + var util2: Util; var sum: int; var num: int; - replaces vals by sum == seqsum2(vals) && num == |vals|; + replaces vals by sum == util2.seqsum(vals) && num == |vals|; refines reset() modifies this; @@ -104,12 +110,6 @@ class CCalc refines ACalc { { m := sum/num; } - - static function method seqsum2(x:seq<int>) : int - decreases x; - { - if (x == []) then 0 else x[0] + seqsum2(x[1..]) - } } // Sequence refined to a singly linked list |