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.

Background¶

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 ( pop ).
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 1.

Popping items from the stack

Here's what should happen if we popped 2 characters off our stack & then clear it.

Note that pop and clear don't unset the Storage array's elements, they just change the value of Last.

Input Format¶

N inputs will be read from stdin/console as inputs, C to the stack.

Constraints¶

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

Output Format¶

If the stack currently has the characters "M", "L", and "H" then the program should print the stack like this:

[M, L, H]

Sample Input¶

M L H d p d p d p d

Sample Output¶

[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;