Running example

In this example, we will write a simple program initializing all the cells of an array to a given value. We start from the procedure receiving as input the array to initialize, the size of the array and the value.

    void init ( int array[ ] , int size , int value ) 
    {
        int i = 0;
        while ( i < size ) 
        {
            array[ i ] = value;
            i = i + 1;
        }
    }
           

Recall that Booster assumes the pass-by-reference paradigm when array variables are given as parameters.

We now want to call the function init from the main:

       #define SIZE
    
           void main( void ) {
             // Declaration of arrays of unknown length is OK for Booster.
             int a[ SIZE ];
             // Uninitialized variables have an unknown value.
             int v;
             
             // call the init procedure
             init( a , SIZE , v );
           }
           

Programs are checked with respect to their assertions. Booster allows specifying standard C assertions and universally quantified assertions. For our example, we want to check that, after the execution of init, the array has been initialized in all its positions from 0 to SIZE. We can specify this property in two ways: (i) a for loop checking every single position of the array or (ii) a quantified assertion. The for-loop is the standard loop we would write in a C program:

       int x;
           for ( x = 0 ; x < SIZE ; x++ ) {
             assert( a[ x ] == v );
           }
           

<span text-align:="" justify;"="">The quantified assertion, instead, offers a more convenient way (both from the user readability perspective and from the verification point of view) to express such property:

       assert( forall (int x) :: ( 0 <= x && x < SIZE ) ==> ( a[ x ] == v ) );
           

The final program will look like this:

       #define SIZE
           
           /*
            * Procedures have to be defined before they are actually called inside other procedures.
            */
    
           void init ( int array[ ] , int size , int value ) {
             int i = 0;
             while ( i < size ) {
               array[ i ] = value;
               i = i + 1;
             }
           }
           
           void main( void ) {
             int a[ SIZE ];
             int v;
             
             init( a , SIZE , v );
    
             assert( forall (int x) :: ( 0 <= x && x < SIZE ) ==> ( a[ x ] == v ) );
           }
           

The execution of Booster on this file (and the default template configuration file) prints the following output:

       # This is booster v0.1 (Beta)
           # Linked to Z3 version 4.3.1.0
           # Random seed for Z3 set to 0
           The program is safe