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 *);
