Let's Build a Stack
In this lab we will build a stack data structure and use the SPARK provers to find the errors in the below implementation.
So, what is a stack?
A stack is like a pile of dishes...
The pile starts out empty.
You add (
push) a new plate (
data) to the stack by placing it on the top of the pile.
To get plates (
data) out, you take the one off the top of the pile (
Out stack has a maximum height (
size) of 9 dishes
Pushing items onto the stack
Here's what should happen if we pushed the string
MLH onto the stack.
The list starts out empty. Each time we push a character onto the stack,
Last increments by
Popping items from the stack
Here's what should happen if we popped
2 characters off our stack & then
clear don't unset the
elements, they just change the value of
N inputs will be read from stdin/console as inputs, C to the stack.
1 <= N <= 1000
C is any character. Characters d and p will be special characters corresponding to the below commands:
p => Pops a character off the stack
d => Prints the current characters in the stack
If the stack currently has the characters "M", "L", and "H" then the program should print the stack like this:
[M, L, H]
M L H d p d p d p d
[M, L, H] [M, L] [M] 
Note that, in order to prove the code below, you need to click on the Prove button. Note also that errors are expected initially — it is up to you to use the output from the prover to correct these and produce a working, fully proved stack!
package Stack with SPARK_Mode => On is procedure Push (V : Character) with Pre => not Full, Post => Size = Size'Old + 1; procedure Pop (V : out Character) with Pre => not Empty, Post => Size = Size'Old - 1; procedure Clear with Post => Size = 0; function Top return Character with Post => Top'Result = Tab(Last); Max_Size : constant := 9; -- The stack size. Last : Integer range 0 .. Max_Size := 0; -- Indicates the top of the stack. When 0 the stack is empty. Tab : array (1 .. Max_Size) of Character; -- The stack. We push and pop pointers to Values. function Full return Boolean is (Last = Max_Size); function Empty return Boolean is (Last < 1); function Size return Integer is (Last); end Stack;package body Stack with SPARK_Mode => On is ----------- -- Clear -- ----------- procedure Clear is begin Last := Tab'First; end Clear; ---------- -- Push -- ---------- procedure Push (V : Character) is begin Tab (Last) := V; end Push; --------- -- Pop -- --------- procedure Pop (V : out Character) is begin Last := Last - 1; V := Tab (Last); end Pop; --------- -- Top -- --------- function Top return Character is begin return Tab (1); end Top; end Stack;with Ada.Command_Line; use Ada.Command_Line; with Ada.Text_IO; use Ada.Text_IO; with Stack; use Stack; procedure Main with SPARK_Mode => Off is ----------- -- Debug -- ----------- procedure Debug is begin if not Stack.Empty then Put ("["); for I in Stack.Tab'First .. Stack.Size - 1 loop Put (Stack.Tab (I) & ", "); end loop; Put_Line (Stack.Tab (Stack.Size) & "]"); else Put_Line (""); end if; end Debug; S : Character; begin ---------- -- Main -- ---------- for Arg in 1 .. Argument_Count loop if Argument (Arg)'Length /= 1 then Put_Line (Argument (Arg) & " is an invalid input to the stack."); else S := Argument (Arg)(Argument (Arg)'First); if S = 'd' then Debug; elsif S = 'p' then if not Stack.Empty then Stack.Pop (S); else Put_Line ("Nothing to Pop, Stack is empty!"); end if; else if not Stack.Full then Stack.Push (S); else Put_Line ("Could not push '" & S & "', Stack is full!"); end if; end if; end if; end loop; end Main;