Site hosted by Angelfire.com: Build your free website today!

interface

type Queue = (* abstract *);

procedure Init (var q: Queue);
(* pre: true
post: s is empty (Size(q) = 0) *)

function Size (q: Queue): integer;
(* pre: true (no precondition)
post: Size(q) is ‘number of elements in queue q’ *) 
procedure Add (var q: Queue; x: String);
(* pre: ‘q not full’
post: ‘x has been added to back of queue q’ *)

procedure Remove (var q: Queue; var x: String);
(* pre: q not empty (Size(q) <> 0)
post: ‘x has been removed from front of q’ *)

const capacity = 9; { Set 9 for this example, it can be any number }
type Queue = record 
front, (* where value is Removed *)
back, (* where value is Added *)
len: 0 .. capacity;
content: array [0 .. capacity – 1] of String
end;

implementation

procedure Init (var q: Queue);
(* pre: true
post: q is empty (Size(q) = 0) *)
begin
s.front := 0; s.back := 0; s.len := 0
end (* Init *);

function Size (q: Queue): integer;
(* pre: true (no precondition)
post: Size(q) is ‘number of elements in stack q’ *) 
begin
Size := q.len
end (* Size *);

procedure Add (var q: Queue; x: String);
(* pre: ‘q not full’
post: ‘x has been added to back of queue q’ *)
begin 
ASSERT(Size(q) <> capacity);
q.content[q.back] := x;
q.back := (q.back + 1) mod capacity; (* ‘wrapping round’ *)
q.len := q.len + 1
end (* Add *);

procedure Remove (var q: Queue; var x: String);
(* pre: q not empty (Size(q) <> 0)
post: ‘x has been removed from front of q’ *)
begin 
ASSERT(Size(q) <> 0);
x := q.content[q.front]; 
q.front := (q.front+1) mod capacity; { wrap round}
q.len := q.len – 1
end (* Remove *);