diff options
Diffstat (limited to 'Test/dafny1')
-rw-r--r-- | Test/dafny1/Answer | 124 | ||||
-rw-r--r-- | Test/dafny1/runtest.bat | 26 |
2 files changed, 0 insertions, 150 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
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat deleted file mode 100644 index f02a7965..00000000 --- a/Test/dafny1/runtest.bat +++ /dev/null @@ -1,26 +0,0 @@ -@echo off
-setlocal
-
-set BINARIES=..\..\Binaries
-set DAFNY_EXE=%BINARIES%\Dafny.exe
-
-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy ExtensibleArrayAuto.dfy BinaryTree.dfy UnboundedStack.dfy SeparationLogicList.dfy ListCopy.dfy ListReverse.dfy ListContents.dfy MatrixFun.dfy pow2.dfy SchorrWaite.dfy SchorrWaite-stages.dfy Cubes.dfy SumOfCubes.dfy FindZero.dfy TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy Induction.dfy Rippling.dfy MoreInduction.dfy Celebrity.dfy BDD.dfy UltraFilter.dfy
-
-rem for %%f in (Queue.dfy PriorityQueue.dfy
-rem ExtensibleArray.dfy ExtensibleArrayAuto.dfy
-rem BinaryTree.dfy
-rem UnboundedStack.dfy
-rem SeparationLogicList.dfy
-rem ListCopy.dfy ListReverse.dfy ListContents.dfy
-rem MatrixFun.dfy pow2.dfy
-rem SchorrWaite.dfy SchorrWaite-stages.dfy
-rem Cubes.dfy SumOfCubes.dfy FindZero.dfy
-rem TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
-rem Induction.dfy Rippling.dfy MoreInduction.dfy
-rem Celebrity.dfy BDD.dfy
-rem UltraFilter.dfy
-rem ) do (
-rem echo.
-rem echo -------------------- %%f --------------------
-rem %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-rem )
|