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.