Contractor Validation Tool

 

Let’s suppose we want to validate the contract of a simple stack with push and pop operations. As we are not interested in the actual elements that are stored, we will use two variables only: one to indicate the next element to be read, and one to indicate the maximum amount of elements allowed.

<variable name="next" type="INT" />

<variable name="max" type="INT" />


A stack constitutes the system that we want to observe and analyze. We need a system invariant that restricts the possible values that the system variables may take.

<contract name="Finite Stack"

        invariant="max > 2 AND next >= -1 AND max > next" >


Important note: variable type specifications, invariants, preconditions and postconditions must be specified in CVC3 format. For more information about this, please refer to its manual.

When we create a stack we determine the maximum amount of elements it may hold.  We require that at least two elements may be stored.

<constructor name="Stack"

        pre="size > 2"

        post="max' = size AND next' = -1" >

    <parameter name="size" type="INT" />

</constructor>


Note that in the postcondition the variables are primed, indicating the value after the execution of the action, in this case the constructor.

Pushing an element requires that the maximum capacity has not yet been reached, and updates the next pointer indicating that a new element is now present.

<action name="push"

        pre="max - 1 > next"

        post="next' = next + 1" >

    <parameter name="elem" type="INT" />

</action>


Note that the parameter elem is ignored in the postcondition since we don’t actually  need to store the data.

Popping requires that the stack has at least one element and updates the next pointer accordingly.

<action name="pop"

        pre="next >= 0"

        post="next' = next - 1" />


Notice that, when modeling contracts, we don’t take into consideration the return value of the actions. We are interested in the effect they produce on the variables.

The full file can be found as Stack.contract in the examples page. It is transcripted here:

<contract name="Finite Stack"

        invariant="max > 2 AND next >= -1 AND max > next" >


    <variable name="next" type="INT" />

    <variable name="max" type="INT" />


    <constructor name="Stack"

            pre="size > 2"

            post="max' = size AND next' = -1" >

        <parameter name="size" type="INT" />

    </constructor>


    <action name="pop"

            pre="next >= 0"

            post="next' = next - 1" />


    <action name="push"

            pre="max - 1 > next"

            post="next' = next + 1" >

        <parameter name="elem" type="INT" />

    </action>

</contract>


After the contract is finished we can validate the contract by running:

contractor -f ltsa Stack.contract


Which will generate a LTSA model of the contract abstraction.

If we want to draw the finite state contract abstraction we can use the graphviz output combined with the graphviz dot tool (which should be installed and accessible by calling ‘dot’).

contractor -o png Stack.contract -f Stack.png


Which produces the following image (named Stack.png):

 

Tutorial 1: Contractor for contract validation