OCL Example: Document software components

The examples above are part of domain models and are used to describe business requirements of the system under construction. OCL can also be used to describe the interfaces of software components. Besides of making the expectations and services of software components more explicit, this is useful for generating code that checks these expectations and services at runtime. This is called 'design by contract' and is the central idea behind the Eiffel programming language.

Let's assume, a developer has to create a stack class based on the following input:

• If an element is added to the stack, it is placed at its top.
• If the stack is empty, retrieving the top element is not possible.
• The operation pop() removes the element, that is in top of the stack and returns this element.

The class could be described like this:

class Stack
{
    Stack();
    Object pop();
    void push(Object anObject);
    Object top();
    int size();
    boolean isEmpty();
}

Now these OCL expressions can be used to describe the classes behaviour:

context Stack::pop(): Object
    pre notEmpty: isEmpty() = false
    post topElementReturned: result = self@pre.top()
    post elementRemoved: size() = self@pre.size() - 1
 
context Stack::top(): Object
    pre notEmpty: isEmpty() = false
 
context Stack::push(anObject: Object): void
    post pushedObjectIsOnTop: top() = anObject