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!