diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 31 | ||||
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 17 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 36 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny1/TerminationDemos.dfy | 22 |
5 files changed, 98 insertions, 10 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 4bdea760..070aa6be 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -198,8 +198,18 @@ Execution trace: (0,0): anon0
SmallTests.dfy(267,19): anon3_Else
(0,0): anon2
+SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon18_Else
+ (0,0): anon11
+ (0,0): anon23_Then
+ (0,0): anon24_Then
+ (0,0): anon15
+ (0,0): anon25_Else
-Dafny program verifier finished with 34 verified, 13 errors
+Dafny program verifier finished with 39 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -464,14 +474,17 @@ Dafny program verifier finished with 8 verified, 2 errors -------------------- NonGhostQuantifiers.dfy --------------------
NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
-NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
-NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
-NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-8 resolution/type errors detected in NonGhostQuantifiers.dfy
+NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
+NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+11 resolution/type errors detected in NonGhostQuantifiers.dfy
-------------------- AdvancedLHS.dfy --------------------
AdvancedLHS.dfy(32,23): Error: target object may be null
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index ea256a58..58e64827 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -33,6 +33,23 @@ class MyClass<T> { (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))
}
+ function method GoodRange(): bool
+ {
+ (forall n | 2 <= n :: 1000 <= n || (exists d | n < d :: d < 2*n)) && (exists K: nat | K < 100 :: true)
+ }
+ function method BadRangeForall(): bool
+ {
+ forall n | n <= 2 :: 1000 <= n || n % 2 == 0 // error: cannot bound range for n
+ }
+ function method BadRangeExists(): bool
+ {
+ exists d | d < 1000 :: d < 2000 // error: cannot bound range for d
+ }
+ function method WhatAboutThis(): bool
+ {
+ forall n :: 2 <= n && (forall M | M == 1000 :: n < M) ==> n % 2 == 0 // error: heuristics don't get this one for n
+ }
+
// Here are more tests
function method F(a: array<T>): bool
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index a839d5a9..ef2049a3 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -272,3 +272,39 @@ class InitCalls { r := new InitCalls.InitFromReference(r); // error, since r.z is unknown
}
}
+
+// --------------- some tests with quantifiers and ranges ----------------------
+
+method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)
+ requires 0 <= N && N <= |a|;
+ requires forall k | 0 <= k && k < N :: a[k] != x;
+ requires exists k | 0 <= k && k < N :: a[k] == y;
+ ensures forall k :: 0 <= k && k < N ==> a[k] != x; // same as the precondition, but using ==> instead of |
+ ensures exists k :: 0 <= k && k < N && a[k] == y; // same as the precondition, but using && instead of |
+{
+ assert x != y;
+}
+
+method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
+ requires 0 <= N && N <= |a|;
+ requires forall k :: 0 <= k && k < N ==> a[k] != x;
+ requires exists k :: 0 <= k && k < N && a[k] == y;
+ ensures forall k | 0 <= k && k < N :: a[k] != x; // same as the precondition, but using | instead of ==>
+ ensures exists k | 0 <= k && k < N :: a[k] == y; // same as the precondition, but using | instead of &&
+{
+ assert x != y;
+}
+
+method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
+ requires 0 <= N && N <= |a|;
+ requires exists k | 0 <= k && k < N :: a[k] == y;
+ ensures forall k | 0 <= k && k < N :: a[k] == y; // error
+{
+ assert N != 0;
+ if (N == 1) {
+ assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k; // in this case, the precondition holds trivially
+ }
+ if (forall k | 0 <= k && k < N :: a[k] == x) {
+ assert x == y;
+ }
+}
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d0eba7cb..0111f9af 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -65,7 +65,7 @@ Dafny program verifier finished with 4 verified, 0 errors -------------------- TerminationDemos.dfy --------------------
-Dafny program verifier finished with 11 verified, 0 errors
+Dafny program verifier finished with 14 verified, 0 errors
-------------------- Substitution.dfy --------------------
diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy index 01a7c7bd..49f5a075 100644 --- a/Test/dafny1/TerminationDemos.dfy +++ b/Test/dafny1/TerminationDemos.dfy @@ -42,6 +42,28 @@ class Ackermann { else
G(m - 1, G(m, n - 1))
}
+
+ function H(m: nat, n: nat): nat
+ {
+ if m == 0 then
+ n + 1
+ else if n == 0 then
+ H(m - 1, 1)
+ else
+ H(m - 1, H(m, n - 1))
+ }
+
+ method ComputeAck(m: nat, n: nat) returns (r: nat)
+ {
+ if (m == 0) {
+ r := n + 1;
+ } else if (n == 0) {
+ call r := ComputeAck(m - 1, 1);
+ } else {
+ call s := ComputeAck(m, n - 1);
+ call r := ComputeAck(m - 1, s);
+ }
+ }
}
// -----------------------------------
|