diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 9 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 15 | ||||
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/FindZero.dfy | 30 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
6 files changed, 57 insertions, 5 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1ac8fc1c..afa88a47 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -483,9 +483,12 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context
-Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context
-10 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context
+13 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index adce71a8..59052ac2 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -121,6 +121,21 @@ class Ghosty { ghost method Theorem(a: int) { }
}
+var SomeField: int;
+
+method SpecialFunctions()
+ modifies this;
+{
+ SomeField := SomeField + 4;
+ var a := old(SomeField); // error: old can only be used in ghost contexts
+ var b := fresh(this); // error: fresh can only be used in ghost contexts
+ var c := allocated(this); // error: allocated can only be used in ghost contexts
+ if (fresh(this)) { // this guard makes the if statement a ghost statement
+ ghost var x := old(SomeField); // this is a ghost context, so it's okay
+ ghost var y := allocated(this); // this is a ghost context, so it's okay
+ }
+}
+
// ---------------------- illegal match expressions ---------------
datatype Tree { Nil; Cons(int, Tree, Tree); }
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 93bd4b65..6b7ce9b9 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -60,7 +60,7 @@ datatype List<T> { Cons(nat, T, List<T>);
}
-method MatchIt(list: List<bool>) returns (k: nat)
+method MatchIt(list: List<object>) returns (k: nat)
{
match (list) {
case Nil =>
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d96e12a5..d0eba7cb 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -59,6 +59,10 @@ Dafny program verifier finished with 2 verified, 0 errors Dafny program verifier finished with 17 verified, 0 errors
+-------------------- FindZero.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
-------------------- TerminationDemos.dfy --------------------
Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy new file mode 100644 index 00000000..cff8b934 --- /dev/null +++ b/Test/dafny1/FindZero.dfy @@ -0,0 +1,30 @@ +method FindZero(a: array<int>) returns (r: int)
+ requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];
+ requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ ensures 0 <= r ==> r < a.Length && a[r] == 0;
+ ensures r < 0 ==> forall i :: 0 <= i && i < a.Length ==> a[i] != 0;
+{
+ var n := 0;
+ while (n < a.Length)
+ invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;
+ {
+ if (a[n] == 0) { r := n; return; }
+ call Lemma(a, n, a[n]);
+ n := n + a[n];
+ }
+ r := -1;
+}
+
+ghost method Lemma(a: array<int>, k: int, m: int)
+ requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];
+ requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+ requires 0 <= k;
+ requires k < a.Length ==> m <= a[k];
+ ensures forall i :: k <= i && i < k+m && i < a.Length ==> a[i] != 0;
+ decreases m;
+{
+ if (0 < m && k < a.Length) {
+ assert a[k] != 0;
+ call Lemma(a, k+1, m-1);
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index b6fc7f62..cab18ddb 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -18,7 +18,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy
MatrixFun.dfy pow2.dfy
SchorrWaite.dfy
- Cubes.dfy SumOfCubes.dfy
+ Cubes.dfy SumOfCubes.dfy FindZero.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
Induction.dfy Rippling.dfy
Celebrity.dfy
|