Previous Up Next

Chapter 2  Tutorial

This chapter provides the basic techniques for specifying a Java source code and prove it correct with Krakatoa. We also recommend to look at the collection of verified programs at URL http://proval.lri.fr/gallery/krakatoa.en.html to get more hints on how to specify and prove programs with Krakatoa.

Before going to the first lesson, we recommend to start by creating a new directory tutorial, and code each example in that directory.

2.1  The basics of the methodology

We start by a very simple static method, that computes the maximum of two integers. In the tutorial sub-directory, write the following Java program into a new file Lesson1.java.

 
public class Lesson1 { 
 
    /*@ ensures \result >= x && \result >= y && 
      @    \forall integer z; z >= x && z >= y ==> z >= \result; 
      @*/ 
    public static int max(int x, int y) { 
        if (x>y) return x; else return x;  
    } 
} 

The comment starting with /*@ just before the method max is a contract specifying a intended behavior for max. The ensures clause introduce a postcondition, which is a formula supposed to hold at end of execution of that method, for any value of its arguments. In that formula,
result denotes the returned value for that method, hence that formula means three things: (i) the result is greater than or equal to x, (ii) the result is also greater than or equal to y, and (iii) the result is the least of all integers both greater than x and y.

Our aim is to verify that the body of method max is a correct implementation, in the sense that it satisfies the contract given. Indeed, we intentionally made a mistake: the second return should return y instead of x.

Running the verification process can be done by executing the following command, in the directory tutorial: 

krakatoa Lesson1.java

The command will read the given file, and generate a set of logic formulas call verification conditions (abbreviated as VC), which express the validity of the program. The generated formulas are then displayed into the graphical interface of the Why3 platform, as shown in Figure 2.1

Figure 2.1: Verification conditions displayed in Why3 IDE

Please refer to Why3’s user manual for details on the use of this interface. We only remind here the main features.

The column on the left is a tool bar. The large window in the middle is the tree view of all generated VCs. There are 4 VCs generated from this program, given as sub-rows of the row called “WP Jessie program”. Generally speaking, there is one VCs for each behavior of each method or constructor. Safety is one of these behaviors, which includes checking absence of null dereferencing, absence of out-of-bounds array acces, absence of division by zero, and other kind of possible runtime errors like that. In this tree view, the first VC has been selected was selected, by clicking on the corresponding row. The corresponding specification frim the source code is shown on the bottom right part: it is here the post-condition we gave to method max. The top right part of the window displays the logical formula associated to the VC.

The left toolbar contains a series of buttons for each prover that was detected when you run “why3config –detect”. A given prover can be run on a given goal, or a set of goals by selecting the wanted part of the tree. In our example, we can select the row “WP Jessie program” and click e.g on Alt-Ergo. Clicking further on other provers like Z3 or CVC3, will run these on the VCs that are not yet proved (see Why3 manual for details). The result is displayed on Figure 2.2.

Figure 2.2: Provers run on verification conditions

The VC for the post-condition of max is not proved. To investigate further, and since it is a conjunction of several propositions, it is a good idea to split it in parts. This is done by selecting the VC and clicking on the “split” button. This results into two subgoals for that VC. Again, we can click on provers Alt-Ergo, Z3 and CVC3 to check these subgoals. The second remains unproved. It can be splitted in parts again, which this time results into 3 subgoals, and provers can be run again on them. The result is displayed on Figure 2.3.

Figure 2.3: Splitting verification condition in parts

The subgoal that remains unproved was selected, and the corresponging spec is shown on the bottom left: it is the part \result >= y which is not valid. Indeed, this comes from our intentional mistake; the result s not necessarily greater or equal to y in the second branch. It is time to fix the source code. You can quit the graphical interface, and replace with your favorite editor the last x by y. If you rerun the krakatoa command as above, you will see that the state of your proof session was recorded and thus see all the splitting you made earlier. You notice also that most of the goals are marked as “obsolete” meaning that the results recorded in your proof sessions are not accurate any more. It is the right time to use the “replay” button of the interface to rerun prover on all obsolete proofs. Then click on the remaining VC and on a prover like Alt-ergo, to see that this time the proof is OK. Indeed, the splittings that you made to reach this state are not necessary anymore; select the first split and the “remove” button, then restart provers on the first VC, it should be proved. This means that the method implementation now satisfies its specification.

2.2  Loop invariants

Methods get a bit harder to prove in presence of loops. Below is a contract of a method for computing the square root of an integer (rounded towards zero).

/*@ requires x >= 0; 
  @ ensures  
  @   \result >= 0 && \result * \result <= x  
  @   && x < (\result + 1) * (\result + 1); 
  @*/ 
public static int sqrt(int x); 

The new requires introduce a precondition. This is formula that is supposed to hold at the beginning of the method call, here we ask for the parameter x to be non-negative, otherwise computing its square root would not be possible. The precondition is not something guaranteed by the method itself: it has to be checked by the caller of the method.

The ensures clause given states now that (i) the result is non-negative, (ii) the square of the result is less than or equal to x, and (iii) the successor of the result has a square which is greater than x. This ensures that the result is indeed the square root rounded towards zero.

To implement such a method, we propose an algorithm based on the following remark: we know that

k−1
∑
i=0
 2i+1 = k2

so the square root of n is the smallest integer k such that

k
∑
i=0
 2i+1

is greater than n.

Now, add the following to your class Lesson1.

/*@ requires x >= 0; 
  @ ensures  
  @   \result >= 0 && \result * \result <= x  
  @   && x < (\result + 1) * (\result + 1); 
  @*/ 
public static int sqrt(int x) { 
    int count = 0, sum = 1; 
    while (sum <= x) {  
        count++; 
        sum = sum + 2*count+1; 
    } 
    return count; 
}    

If you generate the VCs now, using 

krakatoa Lesson1.java

you will see the VC for the post-condition, as shown on Figure 2.4 is unproved. (Please ignore the VC “Safety” for the moment.)

Figure 2.4: Verification conditions for sqrt

Indeed, as usual in Floyd-Hoare logic, to prove a program with a loop it is required to add a loop invariant to have enough information. Finding the right invariant is usually hard, and usually follows from the principle of the algorithm. Here, count will increase one by one, whereas sum will always be the sum of odd integers between 1 and 2*count+1, that is (count+1)*(count+1). So we suggest the following

public static int sqrt(int x) { 
    int count = 0, sum = 1; 
    /*@ loop_invariant 
      @   count >= 0 && x >= count*count && 
      @   sum == (count+1)*(count+1); 
      @*/ 
    while (sum <= x) { 
        count++; 
        sum = sum + 2*count+1; 
    } 
    return count; 
} 
 

If you rerun the krakatoa tool, you should now see that CVC3 and Z3 are able to prove the normal behevior of the method.

Safety

Figure 2.5: Safety VCs for sqrt

Let’s now look at the “Safety” section of VCs. This section contains VCs for checking that no runtime error may occur during execution. These includes:

To understand why safety is not proved, let’s first split the goal and try provers on sub-goals. On this example, arithmetic overflow is the concern. On Figure 2.5, the focus is put on the VC corresponding to expression sum+2*count in the source code (bottom right windows). Looking at the top right window, the goal to prove, which is 

(- 2147483648) <= (integer_of_int32 sum + integer_of_int32 result3)
               <= 2147483647

The constant 2147483648 is 231. This goal amounts to prove that the mathematical result of sum + 2*count fits into the int type. Indeed it is not provable, because it is not always true: if the value of x is too large, arithmetic overflow may occur.

It is possible to find a bound for x, to be added in the precondition, together with appropriate bounds for sum and count to be added as loop invariants, to prove the absence of arithmetic overflow. This is left as an exercise. In some situation, one may want to simply ignore possible arithmetic overflow. This is done by added the following pragma at the beginning of the file:

//@+ CheckArithOverflow = no 

You may try this now, and checks that the “arithmetic overflow” VCs disappear.

Termination

There is another VC that remains to prove, named “loop variant decreases”. Indded, since the sqrt method body contains a while loop, it is possible that the method execution does not terminate for some of the input. To prove termination, you can add another clause to the loop annotation: a loop_variant clause. An integer expression must follow, which is supposed to decreases at each loop iteration, and remaining non-negative. On the sqrt example, that x-sum is decreasing, so you can add:

/*@ loop_invariant  
  @   ... 
  @ loop_variant x − sum; 
  @*/ 
while (sum <= x) {  
   ...

You can check again that this is proved automatically.

2.3  Array accesses

In this lesson, we now consider arrays. You should now create a new file Arrays.java. Here is the specification of a method for computing the maximum element of an array of ints, given as argument:

 
//@+ CheckArithOverflow = no 
 
public class Arrays { 
 
    /*@ requires t != null && t.length >= 1; 
      @ ensures  
      @   0 <= \result < t.length &&  
      @   \forall integer i; 0 <= i < t.length ==> t[i] <= t[\result]; 
      @*/ 
    public static int findMax(int[] t); 
         
} 

The precondition is necessary to ensure that t is a non-empty array, so that the maximum exists. An alternative would have been to raise an exception in that case, but exceptions will be considered later. We also add the pragma for avoiding arithmetic overflow checking for simplicity, although in that case there will be no overflow problem.

We propose the following code for that method:

  public static int findMax(int[] t) { 
      int m = t[0]; 
      int r = 0; 
      /*@ loop_invariant  
        @   1 <= i && i <= t.length && 0 <= r && r < t.length && 
        @   m == t[r] && \forall integer j; 0<=j && j<i ==> t[j]<=t[r]; 
        @ loop_variant t.length−i; 
        @*/ 
      for (int i=1; i < t.length; i++) { 
          if (t[i] > m) { 
              r = i;  
              m = t[i]; 
          } 
      } 
      return r; 
  } 
 

The loop invariant ensures that r is always the index of the maximum element of t between 0 and i-1. We put also as invariant the facts that r and i remain in the bounds of t.

2.4  Logic predicates

The following example is the same is the previous one. We just introduce a logic predicate to avoid the writing of similar formulas. See also http://proval.lri.fr/gallery/krakatoa.en.html.

 
/*@ predicate is_max{L}(int[] t,integer i,integer l) = 
  @   0 <= i < l && 
  @      \forall integer j; 0 <= j < l ==> t[j] <= t[i] ; 
  @*/ 
 
public class Arrays { 
 
    /*@ requires t != null && t.length >= 1; 
      @ ensures is_max(t,\result,t.length); 
      @*/ 
    public static int findMax2(int[] t) { 
        int m = t[0]; 
        int r = 0; 
        /*@ loop_invariant  
          @   1 <= i <= t.length && m == t[r] && is_max(t,r,i) ; 
          @ loop_variant t.length−i; 
          @*/ 
        for (int i=1; i < t.length; i++) { 
            if (t[i] > m) { 
                r = i;  
                m = t[i]; 
            } 
        } 
        return r; 
    } 
 
}

2.5  Array updates

The following method shifts for one cell to the right the contents of an array. It illustrates the \old and the \at constructs. See also http://proval.lri.fr/gallery/krakatoa.en.html.

public class Arrays { 
 
    /*@ requires t != null; 
      @ ensures  
      @   \forall integer i; 0 < i < t.length ==> t[i] == \old(t[i−1]); 
      @*/ 
    public static void shift(int[] t) { 
        /*@ loop_invariant  
          @   j < t.length && 
          @   (\forall integer i; 0 <= i <= j ==> t[i] == \at(t[i],Pre)) && 
          @   (\forall integer i;  
          @         j < i < t.length ==> t[i] == \at(t[i−1],Pre)); 
          @ loop_variant j; 
          @*/ 
        for (int j=t.length−1 ; j > 0 ; j−−) { 
            t[j] = t[j−1]; 
        } 
    } 
 
} 

2.6  Objects and constructors

It is time to consider true Java objects. Let’s consider the following class that implements a very simple electronic purse. See also http://proval.lri.fr/gallery/krakatoa.en.html.

 
class NoCreditException extends Exception { 
 
    public NoCreditException(); 
 
} 
 
public class Purse { 
     
    public int balance; 
 
    //@ invariant balance_non_negative: balance >= 0; 
 
    /*@ ensures balance == 0; 
      @*/ 
    public Purse() { 
        balance = 0; 
    } 
 
    /*@ requires s >= 0; 
      @ ensures balance == \old(balance)+s; 
      @*/ 
    public void credit(int s) { 
        balance += s; 
    } 
 
    /*@ requires s >= 0 && s <= balance; 
      @ ensures balance == \old(balance) − s; 
      @*/ 
    public void withdraw(int s) { 
        balance −= s; 
    } 
     
}

2.7  Calling subprograms, assigns clauses

See also http://proval.lri.fr/gallery/krakatoa.en.html.

    /*@ public normal_behavior 
      @   ensures \result == 150; 
      @*/ 
    public static int test1() { 
        Purse p = new Purse(); 
        p.credit(100); 
        p.withdraw(50); 
        p.credit(100); 
        return p.balance; 
    } 
    /*@ public normal_behavior 
      @   ensures \result == 150; 
      @*/ 
    public static int test2() { 
        Purse p1 = new Purse(); 
        Purse p2 = new Purse(); 
        p1.credit(100); 
        p2.credit(200); 
        p1.withdraw(50); 
        p2.withdraw(100); 
        return p1.balance+p2.balance; 
    } 
 

These tests cannot be proved, the credit and withdraw methods must be given assigns clauses as follows:

/*@ assigns balance; 
  @ ensures balance == 0; 
  @*/ 
Purse() { 
    balance = 0; 
} 
 
/*@ requires s >= 0; 
  @ assigns balance; 
  @ ensures balance == \old(balance)+s; 
  @*/ 
public void credit(int s) { 
    balance += s; 
} 
 
/*@ requires 0 <= s <= balance; 
  @ assigns balance; 
  @ ensures balance == \old(balance) − s; 
  @*/ 
public void withdraw(int s) { 
    balance −= s; 
} 
 

2.8  Programs with exceptions

See also http://proval.lri.fr/gallery/krakatoa.en.html.

class NoCreditException extends Exception { 
 
    /*@ assigns \nothing; 
      @*/ 
    NoCreditException() {} 
 
} 
 
class Purse { 
 
    /*@ requires s >= 0; 
      @ assigns balance; 
      @ ensures s <= \old(balance) && balance == \old(balance) − s; 
      @ behavior amount_too_large: 
      @   assigns \nothing; 
      @   signals (NoCreditException) s > \old(balance) ; 
      @*/ 
    public void withdraw2(int s) throws NoCreditException { 
        if (balance >= s) { 
            balance = balance − s; 
        } 
        else { 
            throw new NoCreditException(); 
        } 
    } 
 
} 
 
 
 

2.9  The Dutch National Flag problem

See also http://proval.lri.fr/gallery/krakatoa.en.html.

 
//@ predicate is_color(int c) = Flag.BLUE <= c && c <= Flag.RED ; 
 
/*@ predicate is_color_array{L}(int t[]) = 
  @   t != null &&  
  @   \forall integer i; 0 <= i && i < t.length ==> is_color(t[i]) ; 
  @*/ 
 
/*@ predicate is_monochrome{L}(int t[],integer i, integer j, int c) = 
  @   \forall integer k; i <= k && k < j ==> t[k] == c ; 
  @*/ 
 
 
 
class Flag { 
     
    public static final int BLUE = 1, WHITE = 2, RED = 3; 
     
    int t[]; 
    //@ invariant t_non_null: t != null; 
    //@ invariant is_color_array_inv: is_color_array(t); 
 
    /*@ requires 0 <= i <= j <= t.length ; 
      @ behavior decides_monochromatic: 
      @   ensures \result <==> is_monochrome(t,i,j,c); 
      @*/ 
    public boolean isMonochrome(int i, int j, int c) { 
            /*@ loop_invariant i <= k &&  
          @   (\forall integer l; i <= l && l < k ==> t[l]==c); 
              @ loop_variant j − k; 
          @*/ 
        for (int k = i; k < j; k++) if (t[k] != c) return false; 
        return true; 
    } 
 
    /*@ requires 0 <= i < t.length && 0 <= j < t.length; 
      @ behavior i_j_swapped: 
      @   assigns t[i],t[j]; 
      @   ensures t[i] == \old(t[j]) && t[j] == \old(t[i]); 
      @*/ 
    private void swap(int i, int j) { 
        int z = t[i]; 
        t[i] = t[j]; 
        t[j] = z; 
    } 
 
    /*@ behavior sorts: 
      @   assigns t[..]; 
      @   ensures  
      @     (\exists integer b,r; is_monochrome(t,0,b,BLUE) && 
      @                           is_monochrome(t,b,r,WHITE) && 
      @                           is_monochrome(t,r,t.length,RED)); 
      @*/ 
    public void flag() { 
        int b = 0; 
        int i = 0; 
        int r = t.length; 
        /*@ loop_invariant 
          @   is_color_array(t) && 
          @   0 <= b && b <= i && i <= r && r <= t.length && 
          @   is_monochrome(t,0,b,BLUE) && 
          @   is_monochrome(t,b,i,WHITE) && 
          @   is_monochrome(t,r,t.length,RED); 
          @ loop_variant r − i;  
          @*/ 
        while (i < r) { 
            switch (t[i]) { 
            case BLUE:   
                swap(b++, i++); 
                break;             
            case WHITE:  
                i++;  
                break; 
            case RED:  
                swap(−−r, i); 
                break; 
            } 
        } 
    } 
} 
 

2.10  Ghost variables

The following example illustrates code instrumentation using ghost variables. See also http://proval.lri.fr/gallery/krakatoa.en.html.

/* complements for non−linear integer arithmetic */ 
 
/*@ lemma distr_right:  
  @   \forall integer x y z; x*(y+z) == (x*y)+(x*z);  
  @*/ 
 
/*@ lemma distr_left:  
  @   \forall integer x y z; (x+y)*z == (x*z)+(y*z); 
  @*/ 
 
/*@ lemma distr_right_minus:  
  @   \forall integer x y z; x*(y−z) == (x*y)−(x*z);  
  @*/ 
 
/*@ lemma distr_left_minus:  
  @   \forall integer x y z; (x−y)*z == (x*z)−(y*z); 
  @*/ 
 
/*@ lemma mul_comm:  
  @   \forall integer x y; x*y == y*x;  
  @*/ 
 
/*@ lemma mul_assoc:  
  @   \forall integer x y z; x*(y*z) == (x*y)*z;  
  @*/ 
 
/*@ predicate divides(integer x, integer y) = 
  @   \exists integer q; y == q*x ; 
  @*/ 
 
/*@ lemma div_mod_property: 
  @  \forall integer x y;  
  @    x >=0 && y > 0 ==> x%y  == x − y*(x/y);   
  @*/ 
 
/*@ lemma mod_property: 
  @  \forall integer x y;  
  @    x >=0 && y > 0 ==> 0 <= x%y && x%y < y;  
  @*/ 
 
/*@ predicate isGcd(integer a, integer b, integer d) = 
  @   divides(d,a) && divides(d,b) &&  
  @     \forall integer z; 
  @     divides(z,a) && divides(z,b) ==> divides(z,d) ; 
  @*/ 
 
/*@ lemma gcd_zero : 
  @   \forall integer a; isGcd(a,0,a) ; 
  @*/ 
 
/*@ lemma gcd_property : 
  @   \forall integer a b d q; 
  @      b > 0 && isGcd(b,a % b,d) ==> isGcd(a,b,d) ; 
  @*/ 
 
class Gcd { 
 
    /*@ requires x >= 0 && y >= 0; 
      @ behavior resultIsGcd:  
      @   ensures isGcd(x,y,\result) ; 
      @ behavior bezoutProperty: 
      @   ensures \exists integer a,b; a*x+b*y == \result; 
      @*/ 
    int gcd(int x, int y) { 
 
        //@ ghost integer a = 1, b = 0, c = 0, d = 1; 
 
        /*@ loop_invariant  
          @    x >= 0 && y >= 0 &&   
          @    (\forall integer d ;  isGcd(x,y,d) ==>  
          @        isGcd(\at(x,Pre),\at(y,Pre),d)) &&  
          @    a*\at(x,Pre)+b*\at(y,Pre) == x &&  
          @    c*\at(x,Pre)+d*\at(y,Pre) == y ; 
          @ loop_variant y; 
          @*/ 
        while (y > 0) { 
            int r = x % y; 
            //@ ghost integer q = x / y; 
            x = y; 
            y = r; 
            //@ ghost integer ta = a, tb = b; 
            //@ ghost a = c;  
            //@ ghost b = d; 
            //@ ghost c = ta − c * q; 
            //@ ghost d = tb − d * q; 
        } 
 
        return x; 
    } 
 
} 
 
Previous Up Next