diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 37 | ||||
| -rw-r--r-- | Test/dafny0/BadFunction.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
3 files changed, 36 insertions, 16 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index ae2aa454..f77d2fd4 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -12,23 +12,23 @@ class MyClass<T, U> { ensures t == t;
ensures old(null) != this;
{
- x := 12;
- while (x < 100)
- invariant x <= 100;
- {
- x := x + 17;
- if (x % 20 == 3) {
- x := this.x + 1;
- } else {
- this.x := x + 0;
- }
- call t, u, v := M(true, lotsaObjects)
- var to: MyClass<T,U>;
- call to, u, v := M(true, lotsaObjects)
- call to, u, v := to.M(true, lotsaObjects)
- assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
+ x := 12;
+ while (x < 100)
+ invariant x <= 100;
+ {
+ x := x + 17;
+ if (x % 20 == 3) {
+ x := this.x + 1;
+ } else {
+ this.x := x + 0;
}
+ call t, u, v := M(true, lotsaObjects)
+ var to: MyClass<T,U>;
+ call to, u, v := M(true, lotsaObjects)
+ call to, u, v := to.M(true, lotsaObjects)
+ assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
+ }
function F(x: int, y: int, h: WildData, k: WildData): WildData
{
@@ -285,6 +285,13 @@ Execution trace: Dafny program verifier finished with 16 verified, 2 errors
+-------------------- BadFunction.dfy --------------------
+BadFunction.dfy(6,3): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 2 verified, 1 error
+
-------------------- Queue.dfy --------------------
Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny0/BadFunction.dfy b/Test/dafny0/BadFunction.dfy new file mode 100644 index 00000000..3affaa80 --- /dev/null +++ b/Test/dafny0/BadFunction.dfy @@ -0,0 +1,13 @@ +// The following function gives rise to an inconsistent axiom, except
+// for its CanUseFunctionDefs antecedent, which saves the day.
+function F(x: int): int
+ decreases x;
+{
+ F(x) + 1 // error: does not decrease termination metric
+}
+
+method M()
+{
+ assert F(5) == 0; // no error is generated here, because of the inconsistent axiom
+ assert false; // ditto
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 003566f3..d72b0899 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -18,7 +18,7 @@ for %%f in (BQueue.bpl) do ( )
for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy
- Modules0.dfy Modules1.dfy Queue.dfy ListCopy.dfy
+ Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
|