{ 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 };