Thursday, September 22, 2011

Application of Model-Based Testing to a Stack

Today I would like to go back to basics, and also show how to easily switch the underlying implementation. Some of my most read posts are on applying Model-Based Testing to basic data structures, so why not pick up yet another basic data structure?

This time I’m keeping it ultra-simple: The Stack.

I’m sure we all know what a stack is, but to briefly remind you it’s a LIFO (Last-in, first-out) container. In a classic stack elements are added on top of the stack using the “Push” command and removed from the top one-by-one using “Pop”. When an element is popped it is removed from the stack and returned. It is not possible to reference elements that are not on the top of the stack.

A not-so-classic stack variation contains a “Peek” function that will return the top element of the stack without removing it.

So without further ado let’s jump into modeling!

For the purpose of this post I’ve re-implemented the wheel and written a fixed-size (10) integer based stack:

    public class Stack
        int[] items = new int[10];
        int count = 0;

        public Stack()

        public void Push(int x)
            if (count >= items.Length)
                throw new Exception("Stack overflow");
            for (int i = count; i > 1; i--)
                items[i] = items[i-1];
            items[count++] = x;

        public int Peek()
            return items[0];

        public int Pop()
            if (count <= 0)
                throw new Exception("Popping empty stack");

            int x = items[0];
            for(int i = 0; i < count; i++)
                items[i] = items[i+1];
            return x;

Pretty standard stuff.

For modeling the stack we define the three actions and model them like this:

    class StackModel
        SequenceContainer<int> inputSequence = new SequenceContainer<int>();

        [Rule(Action = "new this.Stack()")]

        [Rule(Action = "this.Push(x)")]
        void PerformPush(int x)
            Condition.IsTrue(inputSequence.Count < 4);

        [Rule(Action = "this.Peek()/result")]
        int PerformPeek()
            Condition.IsTrue(inputSequence.Count > 0);
            return inputSequence[inputSequence.Count - 1];

        [Rule(Action = "this.Pop()/result")]
        int PerformPop()
            Condition.IsTrue(inputSequence.Count > 0);
            int x = inputSequence[inputSequence.Count - 1];
            inputSequence.RemoveAt(inputSequence.Count - 1);
            return x;

In the config.cord script I have limited the input values for the “Push” action to 0 and 1. Also the model is limited to having at most 3 elements in the stack at any given time.

Exploration of this model yields:

Test cases
There’s an interesting fact about our model. Because every state is connected to all other states, traversing the graph with the “Long tests” strategy will yield only one test case. I don’t like this, so I’m going to change it to use “Short tests” strategy instead.

The generated test cases are:

An interesting fact is that I found two bugs in my implementation of the stack when running these generated tests (that tells you a bit about my coding skills – it’s a good thing I’m hired as a tester...):

1.      Off by one error in the loop that shifts elements out
2.      Push was inserting new elements at the bottom of the stack
            for (int i = count; i > 1; i--)
                items[i] = items[i-1];
            items[count++] = x;

I left the bugs in the sample, which you by the way can find in the reference list [1].

Testing .NET class libraries
Okay, so now we have tested that our stack implementation is not working, let’s try something funny! So .NET contains an implementation of a stack in System.Collections.Stack, wouldn’t it be interesting to check that the guys in .NET did a better job than me implementing a stack? Actually, SpecExplorer allows us to test any .NET class directly. We simply change the using declaration in the config.cord file:

using System.Collections;
//using StackModel.Sample;

And the type binding in the StackModel.cs file:


And re-generate our test suite. The model obviously stays the same (we didn’t change that) but the tests will now call into the .NET stack class implementation.

But wait a minute? We implemented an integer based stack, and the .NET stack holds any objects, then why does this work? It turns out that because the interface for our stack is a subset of that of the more generic .NET stack class, SpecExplorer can automatically cast the arguments from integers to Objects, and everything works out-of-the-box! That is pretty sweet.

Big surprise, running the generated test cases, they all pass! Kudos to the .NET guys for a good job, and I think I will stay on the testing path for now J

And finally I would really appreciate some feedback, so if you made it all the way down here, please leave a comment telling me what you think was good/bad about this post - thanks!

[1] Stack Model


  1. Hi,

    I liked it a lot. It will be good if there is a discussion on multiple stacks. I think it becomes tricky to create two stacks, for example, inter leave them using |||. The reason is that the universal operator (_) may not make sure all instances of stacks are used during exploration. Do you have any comments or thoughts on multiple instance of stacks and interleave them to invoke methods of the Stack class?

    1. I think you have to be careful when to choose instance based modeling over static models (like this stack model for example is static). In this example where I'm testing a stack in isolation, you don't really benefit from doing instance based modeling because the individual instaces wouldn't interact.

      Where it makes sense to do instance based modeling, is if you are modeling a _system_ that comprises multiple stacks. Here the focus shifts from testing the stacks in isolation, to testing the system of inter-dependent stacks. One example where you might have multiple stacks. You could think of a system with multiple bins defining a work-flow, these bins could be represented by stacks, items would then move from one bin to another. Some interesting invariants that a model could check would be conservation of items, meaning that the sum of number of items should be constant, as items cannot disappear in this system. Then the model would consist of all actions/rules that are implemented to move items around... anyway, the point being now we are testing the actual system and no longer the stacks in isolation, and we would thus define system invariants for purpose of validation.