diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-12 13:53:03 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-12 13:53:03 -0700 |
| commit | 4977e01decc2823eda691acea9bbbe7e537c14dc (patch) | |
| tree | 93461a8517756494f744ea4d094eed4e71989737 | |
| parent | 84cd85ffd3c722278eb22d0bf402caf0f717a150 (diff) | |
Dafny: beefed up allocation axioms for boxes stored in fields
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 5 | ||||
| -rw-r--r-- | Test/dafny2/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny2/TreeFill.dfy | 27 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 2 |
4 files changed, 37 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 742fd4e4..fef8fe1f 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -558,6 +558,11 @@ axiom (forall x: int, h: HeapType :: axiom (forall r: ref, h: HeapType ::
{ GenericAlloc($Box(r), h) }
$IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));
+// boxes in the heap
+axiom (forall r: ref, f: Field BoxType, h: HeapType ::
+ { GenericAlloc(read(h, r, f), h) }
+ $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>
+ GenericAlloc(read(h, r, f), h));
// ---------------------------------------------------------------
// -- Arrays -----------------------------------------------------
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 9f7fad4e..b0bbfe05 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -31,6 +31,10 @@ Dafny program verifier finished with 23 verified, 0 errors Dafny program verifier finished with 5 verified, 0 errors
+-------------------- TreeFill.dfy --------------------
+
+Dafny program verifier finished with 3 verified, 0 errors
+
-------------------- StoreAndRetrieve.dfy --------------------
Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy new file mode 100644 index 00000000..f7e2cc89 --- /dev/null +++ b/Test/dafny2/TreeFill.dfy @@ -0,0 +1,27 @@ +datatype Tree<T> = Null | Node(Tree, T, Tree);
+
+function Contains<T>(t: Tree, v: T): bool
+{
+ match t
+ case Null => false
+ case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)
+}
+
+method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)
+ requires a != null && 0 <= start <= a.Length;
+ modifies a;
+ ensures start <= end <= a.Length;
+ ensures forall i :: 0 <= i < start ==> a[i] == old(a[i]);
+ ensures forall i :: start <= i < end ==> Contains(t, a[i]);
+{
+ match (t) {
+ case Null =>
+ end := start;
+ case Node(left, x, right) =>
+ end := Fill(left, a, start);
+ if (end < a.Length) {
+ a[end] := x;
+ end := Fill(right, a, end + 1);
+ }
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 494a8721..794b7908 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -14,7 +14,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
- Intervals.dfy
+ Intervals.dfy TreeFill.dfy
StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy
) do (
echo.
|