summaryrefslogtreecommitdiff
path: root/Test/dafny1/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny1/Answer')
-rw-r--r--Test/dafny1/Answer124
1 files changed, 0 insertions, 124 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
deleted file mode 100644
index e60451c2..00000000
--- a/Test/dafny1/Answer
+++ /dev/null
@@ -1,124 +0,0 @@
-
--------------------- Queue.dfy --------------------
-
-Dafny program verifier finished with 22 verified, 0 errors
-
--------------------- PriorityQueue.dfy --------------------
-
-Dafny program verifier finished with 24 verified, 0 errors
-
--------------------- ExtensibleArray.dfy --------------------
-
-Dafny program verifier finished with 11 verified, 0 errors
-
--------------------- ExtensibleArrayAuto.dfy --------------------
-
-Dafny program verifier finished with 11 verified, 0 errors
-
--------------------- BinaryTree.dfy --------------------
-
-Dafny program verifier finished with 24 verified, 0 errors
-
--------------------- UnboundedStack.dfy --------------------
-
-Dafny program verifier finished with 12 verified, 0 errors
-
--------------------- SeparationLogicList.dfy --------------------
-
-Dafny program verifier finished with 16 verified, 0 errors
-
--------------------- ListCopy.dfy --------------------
-
-Dafny program verifier finished with 4 verified, 0 errors
-
--------------------- ListReverse.dfy --------------------
-
-Dafny program verifier finished with 2 verified, 0 errors
-
--------------------- ListContents.dfy --------------------
-
-Dafny program verifier finished with 9 verified, 0 errors
-
--------------------- MatrixFun.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
-
--------------------- pow2.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
-
--------------------- SchorrWaite.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- SchorrWaite-stages.dfy --------------------
-
-Dafny program verifier finished with 16 verified, 0 errors
-
--------------------- Cubes.dfy --------------------
-
-Dafny program verifier finished with 2 verified, 0 errors
-
--------------------- SumOfCubes.dfy --------------------
-
-Dafny program verifier finished with 17 verified, 0 errors
-
--------------------- FindZero.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
-
--------------------- TerminationDemos.dfy --------------------
-
-Dafny program verifier finished with 14 verified, 0 errors
-
--------------------- Substitution.dfy --------------------
-
-Dafny program verifier finished with 12 verified, 0 errors
-
--------------------- TreeDatatype.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- KatzManna.dfy --------------------
-
-Dafny program verifier finished with 6 verified, 0 errors
-
--------------------- Induction.dfy --------------------
-
-Dafny program verifier finished with 33 verified, 0 errors
-
--------------------- Rippling.dfy --------------------
-
-Dafny program verifier finished with 141 verified, 0 errors
-
--------------------- MoreInduction.dfy --------------------
-MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.
-Execution trace:
- (0,0): anon0
-
-Dafny program verifier finished with 15 verified, 4 errors
-
--------------------- Celebrity.dfy --------------------
-
-Dafny program verifier finished with 10 verified, 0 errors
-
--------------------- BDD.dfy --------------------
-
-Dafny program verifier finished with 5 verified, 0 errors
-
--------------------- UltraFilter.dfy --------------------
-
-Dafny program verifier finished with 19 verified, 0 errors