{ Code taken from Lecture 2 in Data Structures Semester 2 2005 by Mr. Chris Cox }
type Stack = (* abstract *);
procedure Init (var s: Stack);
{ pre: true
post: s is empty (Size(s) = 0) }
function Size (s: Stack): integer;
{ pre: true (no precondition)
post: Size(s) is ‘number of elements in stack s’ }
function Empty (s: Stack): boolean;
{ pre: none
post: ‘returns True if s is empty’ }
procedure Push (var s: Stack; x: string[7]);
{ pre: ‘s not full’
post: ‘x has been added to top of stack s’ }
procedure Pop (var s: Stack; var x: string[7]);
{ pre: s not empty ( Size(s)>0 )
post: x has been removed from top (same end) of s }
const capacity = 13; { This can be any number }
type Stack = record
top: 0 .. capacity;
content: array [1 .. capacity] of string[7]
end;
procedure Init (var s: Stack);
(* pre: true
post: s is empty (Size(s) = 0) *)
begin
s.top := 0
end (* Init *);
function Size (s: Stack): integer;
{ pre: true (no precondition)
post: Size(s) is ‘number of elements in stack s’ }
begin
Size := s.top
end (* Size *);
function Empty (s: Stack): boolean;
{ pre: none
post: ‘returns True if s is empty’ }
begin
Empty := (s.top=0)
end (* Empty *);
procedure Push (var s: Stack; x: string[7]);
(* pre: ‘s not full’
post: ‘x has been added to top of stack s’ *)
begin
ASSERT(s.top < capacity);
s.top := s.top + 1;
s.content[s.top] := x
end (* Push *);
procedure Pop (var s: Stack; var x: string[7]);
{pre: s not empty (Size(s) > 0)
post:‘x has been removed from top (same end) of s’ }
begin
ASSERT( s.top>0 );
x := s.content[s.top];
s.top := s.top – 1
end { Pop };