diff options
| author |  rustanleino <unknown> | 2010-12-10 20:12:01 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-12-10 20:12:01 +0000 |
| commit | 388982a26093f3e2415572578ac3124dd4245a7e (patch) | |
| tree | 9e0cd8a90dcf70da9b6e9a924aa577c9decb5858 | |
| parent | 04468d4b9b7d460045350f6c65a3f223c716b553 (diff) | |
Dafny: Added Test/dafny1/PriorityQueue.dfy
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/PriorityQueue.dfy | 111 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
3 files changed, 116 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 8742414b..b8f9591f 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -7,6 +7,10 @@ Boogie program verifier finished with 8 verified, 0 errors Dafny program verifier finished with 22 verified, 0 errors
+-------------------- PriorityQueue.dfy --------------------
+
+Dafny program verifier finished with 12 verified, 0 errors
+
-------------------- BinaryTree.dfy --------------------
Dafny program verifier finished with 24 verified, 0 errors
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy new file mode 100644 index 00000000..76e4b1d6 --- /dev/null +++ b/Test/dafny1/PriorityQueue.dfy @@ -0,0 +1,111 @@ +class PriorityQueue {
+ var N: int; // capacity
+ var n: int; // current size
+ ghost var Repr: set<object>; // set of objects that make up the representation of a PriorityQueue
+
+ var a: array<int>; // private implementation of PriorityQueu
+
+ function Valid(): bool
+ reads this, Repr;
+ {
+ MostlyValid() &&
+ (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+ }
+
+ function MostlyValid(): bool
+ reads this, Repr;
+ {
+ this in Repr && a in Repr &&
+ a != null && a.Length == N+1 &&
+ 0 <= n && n <= N
+ }
+
+ method Init(capacity: int)
+ requires 0 <= capacity;
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ ensures N == capacity;
+ {
+ N := capacity;
+ var arr := new int[N+1];
+ a := arr;
+ n := 0;
+ Repr := {this};
+ Repr := Repr + {a};
+ }
+
+ method Insert(x: int)
+ requires Valid() && n < N;
+ modifies this, a;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures n == old(n) + 1 && N == old(N);
+ {
+ n := n + 1;
+ a[n] := x;
+ call SiftUp(n);
+ }
+
+ method SiftUp(k: int)
+ requires 1 <= k && k <= n;
+ requires MostlyValid();
+ requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
+ requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != k ==> a[j/2/2] <= a[j]);
+ modifies a;
+ ensures Valid();
+ {
+ var i := k;
+ assert MostlyValid();
+ while (1 < i)
+ invariant i <= k && MostlyValid();
+ invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+ invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != i ==> a[j/2/2] <= a[j]);
+ {
+ if (a[i/2] <= a[i]) {
+ return;
+ }
+ var tmp := a[i]; a[i] := a[i/2]; a[i/2] := tmp;
+ i := i / 2;
+ }
+ }
+
+ method RemoveMin() returns (x: int)
+ requires Valid() && 1 <= n;
+ modifies this, a;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures n == old(n) - 1;
+ {
+ x := a[1];
+ a[1] := a[n];
+ n := n - 1;
+ call SiftDown(1);
+ }
+
+ method SiftDown(k: int)
+ requires 1 <= k;
+ requires MostlyValid();
+ requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
+ requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
+ modifies a;
+ ensures Valid();
+ {
+ var i := k;
+ while (2*i <= n) // while i is not a leaf
+ invariant 1 <= i && MostlyValid();
+ invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+ invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
+ {
+ var smallestChild;
+ if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
+ smallestChild := 2*i + 1;
+ } else {
+ smallestChild := 2*i;
+ }
+ if (a[i] <= a[smallestChild]) {
+ return;
+ }
+ var tmp := a[i]; a[i] := a[smallestChild]; a[smallestChild] := tmp;
+ i := smallestChild;
+ assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];
+ }
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 8a21b3d8..af1cd7bf 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -11,7 +11,7 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f
)
-for %%f in (Queue.dfy
+for %%f in (Queue.dfy PriorityQueue.dfy
BinaryTree.dfy
UnboundedStack.dfy
SeparationLogicList.dfy
|