diff options
Diffstat (limited to 'Test/VSComp2010/Problem5-DoubleEndedQueue.dfy')
| -rw-r--r-- | Test/VSComp2010/Problem5-DoubleEndedQueue.dfy | 163 |
1 files changed, 0 insertions, 163 deletions
diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy deleted file mode 100644 index 0e141927..00000000 --- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy +++ /dev/null @@ -1,163 +0,0 @@ -// VSComp 2010, problem 5, double-ended queue.
-// Rustan Leino, 18 August 2010.
-//
-// This program employs the standard Valid()/Repr idiom used in the dynamic-frames
-// style of specifications, see for example the comment in Problem3-FindZero.dfy.
-// Within that idiom, the specification is straightforward (if verbose), and there
-// are no particular wrinkles or annoyances in getting the verifier to prove the
-// correctness.
-
-class AmortizedQueue<T> {
- // The front of the queue.
- var front: LinkedList<T>;
- // The rear of the queue (stored in reversed order).
- var rear: LinkedList<T>;
-
- ghost var Repr: set<object>;
- ghost var List: seq<T>;
-
- function Valid(): bool
- reads this, Repr;
- {
- this in Repr &&
- front != null && front in Repr && front.Repr <= Repr && front.Valid() &&
- rear != null && rear in Repr && rear.Repr <= Repr && rear.Valid() &&
- |rear.List| <= |front.List| &&
- List == front.List + rear.ReverseSeq(rear.List)
- }
-
- method Init()
- modifies this;
- ensures Valid() && List == [];
- {
- front := new LinkedList<T>.Init();
- rear := new LinkedList<T>.Init();
- Repr := {this};
- Repr := Repr + front.Repr + rear.Repr;
- List := [];
- }
-
- method InitFromPieces(f: LinkedList<T>, r: LinkedList<T>)
- requires f != null && f.Valid() && r != null && r.Valid();
- modifies this;
- ensures Valid() && List == f.List + r.ReverseSeq(r.List);
- {
- if (r.length <= f.length) {
- front := f;
- rear := r;
- } else {
- var rr := r.Reverse();
- var ff := f.Concat(rr);
- front := ff;
-
- rear := new LinkedList<T>.Init();
- }
- Repr := {this};
- Repr := Repr + front.Repr + rear.Repr;
- List := front.List + rear.ReverseSeq(rear.List);
- }
-
- method Front() returns (t: T)
- requires Valid() && List != [];
- ensures t == List[0];
- {
- t := front.head;
- }
-
- method Tail() returns (r: AmortizedQueue<T>)
- requires Valid() && List != [];
- ensures r != null && r.Valid() && r.List == List[1..];
- {
- r := new AmortizedQueue<T>.InitFromPieces(front.tail, rear);
- }
-
- method Enqueue(item: T) returns (r: AmortizedQueue<T>)
- requires Valid();
- ensures r != null && r.Valid() && r.List == List + [item];
- {
- var rr := rear.Cons(item);
- r := new AmortizedQueue<T>.InitFromPieces(front, rr);
- }
-}
-
-
-class LinkedList<T> {
- var head: T;
- var tail: LinkedList<T>;
- var length: int;
-
- ghost var List: seq<T>;
- ghost var Repr: set<LinkedList<T>>;
-
- function Valid(): bool
- reads this, Repr;
- {
- this in Repr &&
- 0 <= length && length == |List| &&
- (length == 0 ==> List == [] && tail == null) &&
- (length != 0 ==>
- tail != null && tail in Repr &&
- tail.Repr <= Repr && this !in tail.Repr &&
- tail.Valid() &&
- List == [head] + tail.List &&
- length == tail.length + 1)
- }
-
- method Init()
- modifies this;
- ensures Valid() && List == [];
- {
- tail := null;
- length := 0;
- List := [];
- Repr := {this};
- }
-
- method Cons(d: T) returns (r: LinkedList<T>)
- requires Valid();
- ensures r != null && r.Valid() && r.List == [d] + List;
- {
- r := new LinkedList<T>;
- r.head := d;
- r.tail := this;
- r.length := length + 1;
- r.List := [d] + List;
- r.Repr := {r} + Repr;
- }
-
- method Concat(end: LinkedList<T>) returns (r: LinkedList<T>)
- requires Valid() && end != null && end.Valid();
- ensures r != null && r.Valid() && r.List == List + end.List;
- decreases Repr;
- {
- if (length == 0) {
- r := end;
- } else {
- var c := tail.Concat(end);
- r := c.Cons(head);
- }
- }
-
- method Reverse() returns (r: LinkedList<T>)
- requires Valid();
- ensures r != null && r.Valid() && |List| == |r.List|;
- ensures (forall k :: 0 <= k && k < |List| ==> List[k] == r.List[|List|-1-k]);
- ensures r.List == ReverseSeq(List);
- decreases Repr;
- {
- if (length == 0) {
- r := this;
- } else {
- r := tail.Reverse();
- var e := new LinkedList<T>.Init();
- e := e.Cons(head);
- r := r.Concat(e);
- }
- }
-
- static function ReverseSeq(s: seq<T>): seq<T>
- {
- if s == [] then [] else
- ReverseSeq(s[1..]) + [s[0]]
- }
-}
|