diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/Answer | 4 | ||||
-rw-r--r-- | Test/dafny0/Counter.dfy | 51 | ||||
-rw-r--r-- | Test/dafny0/Refinement.dfy | 122 | ||||
-rw-r--r-- | Test/dafny0/runtest.bat | 2 |
4 files changed, 125 insertions, 54 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 15986246..c56c2aeb 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -448,6 +448,6 @@ Dafny program verifier finished with 10 verified, 0 errors Dafny program verifier finished with 5 verified, 0 errors
--------------------- Counter.dfy --------------------
+-------------------- Refinement.dfy --------------------
-Dafny program verifier finished with 22 verified, 0 errors
+Dafny program verifier finished with 39 verified, 0 errors
diff --git a/Test/dafny0/Counter.dfy b/Test/dafny0/Counter.dfy deleted file mode 100644 index 63f2fc3c..00000000 --- a/Test/dafny0/Counter.dfy +++ /dev/null @@ -1,51 +0,0 @@ -// Concrete language syntax for a Dafny extension with refinement. -// 6/28/2010 - -class A { - var n : int; - - method Init() modifies this; - { n := 0;} - - method Inc() modifies this; - { n := n + 1;} - - method Dec() - modifies this; - requires n > 0; - { n := n - 1;} - - method Test1(p: int) returns (i: int) - { - assume true; - } - - method Test2() returns (o: object) - { o := this; } -} - -class B refines A { - var inc : int, dec : int; - - replaces n by n == inc - dec; - // transforms n into inc - dec; - - refines Init() modifies this; - { inc := 0; dec := 0;} - - refines Inc() modifies this; - { inc := inc + 1; } - - refines Dec() - modifies this; - requires inc > dec; - { dec := dec + 1; } - - refines Test1(p: int) returns (i: int) - { - i := p; - } -} - - - diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy new file mode 100644 index 00000000..c70df916 --- /dev/null +++ b/Test/dafny0/Refinement.dfy @@ -0,0 +1,122 @@ +// Concrete language syntax for a Dafny extension with refinement. +// Counter example. +// 6/28/2010 + +class A { + var n : int; + + method Init() modifies this; + { n := 0;} + + method Inc() modifies this; + { n := n + 1;} + + method Dec() + modifies this; + requires n > 0; + { n := n - 1;} + + method Test1(p: int) returns (i: int) + { + assume true; + } + + method Test2() returns (o: object) + { o := this; } +} + +class B refines A { + var inc : int, dec : int; + + replaces n by n == inc - dec; + // transforms n into inc - dec; + + refines Init() modifies this; + { inc := 0; dec := 0;} + + refines Inc() modifies this; + { inc := inc + 1; } + + refines Dec() + modifies this; + requires inc > dec; + { dec := dec + 1; } + + refines Test1(p: int) returns (i: int) + { + i := p; + } +} + +// Carrol Morgan's calculator +// 7/2/2010 Kuat + +class ACalc { + var vals: seq<int>; + + method reset() + modifies this; + { + vals := []; + } + + method add(x: int) + modifies this; + { + vals := [x] + vals; + } + + 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..]) + } +} + + +class CCalc refines ACalc { + var sum: int; + var num: int; + replaces vals by sum == seqsum2(vals) && num == |vals|; + + refines reset() + modifies this; + { + sum := 0; + num := 0; + } + + refines add(x: int) + modifies this; + { + sum := sum + x; + num := num + 1; + } + + refines mean() returns (m: int) + requires num > 0; + { + m := sum/num; + } + + static function method seqsum2(x:seq<int>) : int + decreases x; + { + if (x == []) then 0 else x[0] + seqsum2(x[1..]) + } +} + + + + + + + + + diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 8913e626..e238f082 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -14,7 +14,7 @@ for %%f in (Simple.dfy) do ( for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
Termination.dfy Use.dfy DTypes.dfy
- TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Counter.dfy) do (
+ TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
|