diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny2/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 15 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 3 | ||||
| -rw-r--r-- | Test/vstte2012/Answer | 4 | ||||
| -rw-r--r-- | Test/vstte2012/runtest.bat | 3 |
7 files changed, 24 insertions, 11 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index b2876948..06cac03b 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -11,6 +11,10 @@ Dafny program verifier finished with 24 verified, 0 errors 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
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 22bef761..fa7f7c70 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
for %%f in (Queue.dfy PriorityQueue.dfy
- ExtensibleArray.dfy
+ ExtensibleArray.dfy ExtensibleArrayAuto.dfy
BinaryTree.dfy
UnboundedStack.dfy
SeparationLogicList.dfy
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index f359e416..f466d813 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -27,6 +27,10 @@ Dafny program verifier finished with 4 verified, 0 errors Dafny program verifier finished with 23 verified, 0 errors
+-------------------- StoreAndRetrieve.dfy --------------------
+
+Dafny program verifier finished with 22 verified, 0 errors
+
-------------------- Intervals.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index 15c82d65..9ea7a3ff 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -1,4 +1,5 @@ -ghost module A imports Library {
+ghost module A {
+ module L = Library;
class {:autocontracts} StoreAndRetrieve<Thing> {
ghost var Contents: set<Thing>;
predicate Valid
@@ -13,12 +14,12 @@ ghost module A imports Library { {
Contents := Contents + {t};
}
- method Retrieve(matchCriterion: Function) returns (thing: Thing)
- requires exists t :: t in Contents && Function.Apply(matchCriterion, t);
+ method Retrieve(matchCriterion: L.Function) returns (thing: Thing)
+ requires exists t :: t in Contents && L.Function.Apply(matchCriterion, t);
ensures Contents == old(Contents);
- ensures thing in Contents && Function.Apply(matchCriterion, thing);
+ ensures thing in Contents && L.Function.Apply(matchCriterion, thing);
{
- var k :| k in Contents && Function.Apply(matchCriterion, k);
+ var k :| k in Contents && L.Function.Apply(matchCriterion, k);
thing := k;
}
}
@@ -44,9 +45,9 @@ module B refines A { var i := 0;
while (i < |arr|)
invariant i < |arr|;
- invariant forall j :: 0 <= j < i ==> !Function.Apply(matchCriterion, arr[j]);
+ invariant forall j :: 0 <= j < i ==> !L.Function.Apply(matchCriterion, arr[j]);
{
- if (Function.Apply(matchCriterion, arr[i])) { break; }
+ if (L.Function.Apply(matchCriterion, arr[i])) { break; }
i := i + 1;
}
var k := arr[i];
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 19b116d2..25dbed54 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -4,7 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-REM soon again: SnapshotableTrees.dfy StoreAndRetrieve.dfy
+REM soon again: SnapshotableTrees.dfy
for %%f in (
Classics.dfy
TreeBarrier.dfy
@@ -13,6 +13,7 @@ for %%f in ( COST-verif-comp-2011-2-MaxTree-datatype.dfy
COST-verif-comp-2011-3-TwoDuplicates.dfy
COST-verif-comp-2011-4-FloydCycleDetect.dfy
+ StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
) do (
diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer index 15a95de1..bca270c3 100644 --- a/Test/vstte2012/Answer +++ b/Test/vstte2012/Answer @@ -11,6 +11,10 @@ Dafny program verifier finished with 25 verified, 0 errors Dafny program verifier finished with 13 verified, 0 errors
+-------------------- RingBufferAuto.dfy --------------------
+
+Dafny program verifier finished with 13 verified, 0 errors
+
-------------------- Tree.dfy --------------------
Dafny program verifier finished with 15 verified, 0 errors
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat index cda455fa..7f7c9b9f 100644 --- a/Test/vstte2012/runtest.bat +++ b/Test/vstte2012/runtest.bat @@ -4,11 +4,10 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-REM removed for now: RingBufferAuto.dfy
for %%f in (
Two-Way-Sort.dfy
Combinators.dfy
- RingBuffer.dfy
+ RingBuffer.dfy RingBufferAuto.dfy
Tree.dfy
BreadthFirstSearch.dfy
) do (
|