  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;

}

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. A system precondition part that predicates over the list structure.

2. A 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.

return l != 0;

}

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. Which function is the invariant.

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

3. Which 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();" />

<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