Contractor Validation Tool

 

Lets say we have the following C code (named  “List.c”) implementing a singly-linked list.

#include <stdio.h>

#include <stdlib.h>


typedef int boolean;


typedef struct node {

    int data;

    struct node *next;

} node;


typedef struct list {

    int size;

    node* first;

} list;


list* l;


boolean List() {

    l = (list*) malloc(sizeof(list));

    if (l == 0) {

        printf("Error! memory is not available\n");

        return 0;

    }

    l->size = 0;

    l->first = 0;

    return 1;

}


boolean add(int data){

    node *tmp = l->first;

    while (tmp->next != l->first)

        tmp = tmp->next;

    tmp->next = (node*) malloc(sizeof(node));

    if(tmp->next == 0) {

        printf("Error! memory is not available\n");

        l = 0;

        return 0;

    }

    tmp = tmp->next;

    tmp->data = data;

    tmp->next = l->first;

    l->size++;

    return 1;

}


void remove(){

    l->size--;

    node* new_first = l->first->next;

    free(l->first);

    l->first = new_first;

}


void destroy()

{

    node* current;

    node* tmp;

    current = l->first;

    l->first = 0;

    while(current != 0) {

        tmp = current->next;

        free(current);

        current = tmp;

    }

    l = 0;

}


We would like to validate it and see if it has any bugs using Contractor. In order to do so, we will follow 4 steps:

  1. 1.Write an invariant for the list structure.

  2. 2.Write preconditions for each of the actions.

  3. 3.Create a binding file.

  4. 4.Construct an abstraction using Contractor.


Step 1: writing an invariant

Writing an invariant for the list is an easy task, we just need to specify that either l is NULL, or its size attribute is non-negative.

boolean invariant() {

    return l == 0 || l->size >= 0;

}



Step 2: writing preconditions

Writing preconditions is trickier. We need to split the condition for each action into two parts:

  1. BulletA system precondition part that predicates over the list structure.

  2. BulletA parameter precondition part that predicates over the action parameters.

Considering that, since the List action is going to be considered an “initializer”, it will only have a parameter precondition. Furthermore, as it takes no parameters, it is trivial to write:

boolean par_pre_List() {

    return 1;

}


The add operation requires the list structure not to be NULL. It imposes no restriction over the parameter.

boolean sys_pre_add() {

    return l != 0;

}

boolean par_pre_add(int data) {

    return 1;

}


The remove operation is similar but it also requires the list to be not empty.

boolean sys_pre_remove() {

    return l != 0 && l->size > 0;

}

boolean par_pre_remove() {

    return 1;

}


Finally, the destroy operation, which has the same restrictions as adding elements.

boolean sys_pre_destroy() {

    return l != 0;

}

boolean par_pre_destroy() {

    return 1;

}



Step 3: writing a binding file

We now need to write a binding file, which indicates:

  1. BulletWhich function is the invariant.

  2. BulletWhich functions are initializers, together with their preconditions.

  3. BulletWhich other functions are there, together with their preconditions.

So we proceed and create a file named List.binding (which can be found in the examples page):

<code-binding name="List" language="c"

                    file="List.c" inv="return invariant();" >


    <initializer name="List" pre="return sys_pre_List();"

                    params_pre="return par_pre_List();" />


    <function name="add" pre="return sys_pre_add();"

                    params_pre="return par_pre_add(data);" >

            <parameter type="int" name="data" />

    </function>


    <function name="remove" pre="return sys_pre_remove();"

                    params_pre="return par_pre_remove();" />


    <function name="destroy" pre="return sys_pre_destroy();"

                    params_pre="return par_pre_destroy();" />


</code-binding>



Step 4: running Contractor

We must indicate contractor that we are using code with preconditions as input. We will also set a flag in order to get its output in PNG format.

contractor -i code-with-pre -o png List.binding -f List.png



Which will produce the following PNG image (named List.png):

 

Tutorial 2: Contractor for code validation