diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test21/MapAxiomsConsistency.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test21/MapAxiomsConsistency.bpl')
| -rw-r--r-- | Test/test21/MapAxiomsConsistency.bpl | 97 |
1 files changed, 97 insertions, 0 deletions
diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl new file mode 100644 index 00000000..d5344449 --- /dev/null +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -0,0 +1,97 @@ +// Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft.
+// Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy
+
+type ref;
+
+const null: ref;
+
+type Set T = [T]bool;
+function Set#Empty<T>() returns (Set T);
+function Set#Singleton<T>(T) returns (Set T);
+function Set#UnionOne<T>(Set T, T) returns (Set T);
+function Set#Union<T>(Set T, Set T) returns (Set T);
+function Set#Intersection<T>(Set T, Set T) returns (Set T);
+function Set#Difference<T>(Set T, Set T) returns (Set T);
+function Set#Subset<T>(Set T, Set T) returns (bool);
+function Set#Equal<T>(Set T, Set T) returns (bool);
+function Set#Disjoint<T>(Set T, Set T) returns (bool);
+
+type Seq _;
+function Seq#Length<T>(Seq T) returns (int);
+function Seq#Empty<T>() returns (Seq T);
+function Seq#Singleton<T>(T) returns (Seq T);
+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
+function Seq#Append<T>(Seq T, Seq T) returns (Seq T);
+function Seq#Index<T>(Seq T, int) returns (T);
+function Seq#Contains<T>(Seq T, T) returns (bool);
+function Seq#Equal<T>(Seq T, Seq T) returns (bool);
+function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
+function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
+function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+
+type Field _;
+type HeapType = <alpha>[ref,Field alpha]alpha;
+function $IsGoodHeap(HeapType) returns (bool);
+var $Heap: HeapType where $IsGoodHeap($Heap);
+const alloc: Field bool;
+function $HeapSucc(HeapType, HeapType) returns (bool);
+
+const unique Node.list: Field (Seq ref);
+const unique Node.footprint: Field [ref]bool;
+const unique Node.data: Field ref;
+const unique Node.next: Field ref;
+function Node.Valid($heap: HeapType, this: ref) returns (bool);
+
+
+
+
+axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
+
+axiom (forall $Heap: HeapType, this: ref :: { Node.Valid($Heap, this) } this != null && $IsGoodHeap($Heap) ==> Node.Valid($Heap, this) == ($Heap[this, Node.footprint][this] && !$Heap[this, Node.footprint][null] && (forall n: ref :: $Heap[this, Node.footprint][n] ==> $Heap[n, Node.footprint][n] && !$Heap[n, Node.footprint][null] && Set#Subset($Heap[n, Node.footprint], $Heap[this, Node.footprint]) && ($Heap[n, Node.next] == null ==> Seq#Equal($Heap[n, Node.list], Seq#Build(Seq#Empty(), 0, $Heap[n, Node.data], 1))) && ($Heap[n, Node.next] != null ==> $Heap[n, Node.footprint][$Heap[n, Node.next]] && Set#Subset($Heap[$Heap[n, Node.next], Node.footprint], $Heap[n, Node.footprint]) && !$Heap[$Heap[n, Node.next], Node.footprint][n] && Seq#Equal($Heap[n, Node.list], Seq#Append(Seq#Build(Seq#Empty(), 0, $Heap[n, Node.data], 1), $Heap[$Heap[n, Node.next], Node.list])))) && ($Heap[this, Node.next] != null ==> Node.Valid($Heap, $Heap[this, Node.next]))));
+
+
+
+
+procedure Node.ReverseInPlace(this: ref where this != null && $Heap[this, alloc]) returns (reverse: ref where reverse == null || $Heap[reverse, alloc]);
+ // user-defined preconditions
+ free requires Node.Valid($Heap, this);
+ requires $Heap[this, Node.footprint][this];
+ requires !$Heap[this, Node.footprint][null];
+ requires $Heap[this, Node.next] != null ==> Node.Valid($Heap, $Heap[this, Node.next]);
+ modifies $Heap;
+ // frame condition
+ // boilerplate
+ free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure CheckWellformed$$Node.Valid(this: ref where this != null && $Heap[this, alloc]);
+
+
+
+
+
+implementation Node.ReverseInPlace(this: ref) returns (reverse: ref)
+{
+ var current: ref where current == null || $Heap[current, alloc], $PreLoopHeap0: HeapType, nx: ref where nx == null || $Heap[nx, alloc];
+
+ // ----- var-declaration statement ----- test.dfy(28,9)
+ current := $Heap[this, Node.next];
+
+
+ // ----- assignment statement ----- test.dfy(29,13)
+ reverse := this;
+ // ----- assignment statement ----- test.dfy(30,18)
+ $Heap[reverse, Node.next] := null;
+ assume $IsGoodHeap($Heap);
+
+
+
+ // ----- assignment statement ----- test.dfy(31,23)
+ $Heap[reverse, Node.footprint] := // Set#UnionOne(Set#Empty(), reverse);
+ Set#Singleton(reverse);
+
+ assert current == null;
+}
+
+
|