contracts in java

Question

I'm trying to find out more about the meaning of contracts in java.

Here's an example of two contracts in java:

*/
* @pre  arr != null
* @pre  occurrences(4,arr) == occurrences(5, arr)
* @pre  arr[arr.length – 1] != 4
* @pre  forall 0 <= i < arr.length-2, arr[i] == 4 ==> arr[i+1] != 4
* @post forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i]
* @post $ret != arr
* @post permutation(arr, $ret)
* @post forall 0 <= i < arr.length-1, arr[i] == 4 ==> $ret[i] == 4
* @post forall 0 <= i < $ret.length-2, $ret[i] == 4 ==> $ret[i+1] == 5
/

And the second one:

*/
* @post (arr != null AND
*        occurrences(4,arr) == occurrences(5, arr) AND
*       arr[arr.length – 1] != 4 AND
*       forall 0 <= i < arr.length-2, arr[i] == 4 ==> arr[i+1] != 4)
<==        *
*       (forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] AND
*        $ret != arr AND
*        permutation(arr, $ret) AND
*  $ret.length == arr.length AND
*        forall 0 <= i < arr.length-1, arr[i] == 4 ==> $ret[i] == 4 AND
*        forall 0 <= i < $ret.length-2, $ret[i]==4 ==> $ret[i+1] == 5)
/

The mission is to change a given array with those pre-conditions so that after any apperance of 4 will come 5. For examples:

fix45({5,4,9,4,9,5}) -> {9,4,5,4,5,9}

fix45({1,4,1,5}) -> {1,4,5,1}

This is what I wrote (It works):

public static  int pos (int[] arr, int k){

    while (arr[k]!=5){
        k=k+1;
        }
    return k;
}

public static  int[] fix45(int[] arr){
    int k=0;
    for(int i = 0; i<=arr.length-1; i++){
        if (arr[i] == 4){
            int place= pos(arr,k);
            arr[place]=arr[i+1];
            arr[i+1]=5;
            k=k+3;


        }

    }
    return arr;
}

My questins: 1. what is the difference bewteen the two contracts? 2.should I actually chack the pre-conditions? 3. what this "And" means? 4. how my code should change according the second contract?

Thank you guys.

Answer 1

1. What is the difference between the two contracts?

The first one restrict the parameters to the methods in a way that they must met the given preconditions. As an example the arr argument must not be null, otherwise its an error. In the second example however you can pass any arguments you want, but: when the arguments is of some specific layout/structure (not null, got the same number of 4's and 5's, ...) it must return/change the array in such a way to match the conclusion (I believe the arrow at <== * must be turned).

2. should I actually check the pre-conditions

Yes, specially if you say so. Additionally it should be mentioned in a javadoc comment and it should say what happends when it doesn't. Javadoc got the @throws keyword for that. Something like

/**
 * (...)
 * @throws NullPointerException If the argument is <code>null</code>.
 * @throws IllegalArgumentException If the number of 4's and 5's is not the same.
 */

3. what this "And" means?

the AND is a logical conjunction. It evaluates to true if both arguments/statements are true.

4. how my code should change according the second contract?

You should not throw and exceptions or change the array in any way, unless it matches the hypothesis (the part before the ==>). In that case the array (and/or the return value) must be changed according to the conclusion.

Answer 2

I can't claim to know, but here is my interpretation of the given conditions.

First of all, your code does not actually seem to follow either contract. It violates the $ret != arr and forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] conditions.

1. Because both conditions require you to not mutate arr (via the forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] postcondition, and all of the conditions (pre and post) in the first are post conditions in the second, the contracts are the same The first requires errors to be throw if the preconditions are not met. The second means you should simply return something (such as null or arr or any other value) if arr is null or otherwise not valid.

2. You probably should throw an illegal argument exception when the preconditions are violated (but perhaps you should talk to the person giving you the contract about that).

3. I assume AND logically ands the conditions together, just as if they had been described separately (but can be used in conjunction with ORs for more flexibility)

4. It shouldn't need to. Instead of throwing an IllegalArgumentException when the preconditions are not met, return null

Edit For Comments:

I believe $ret != arr means that the return value can not refer to the same int[] as arr. That is, you must create a new int[] somewhere in your function and return that.

forall 0 <= i < arr.length-1, $prev(arr[i]) == arr[i] means that every element of arr (except the last one for some reason) must be the same as it was previously (before the function was called). i.e. you can't mutate it (much). This is consistent with requiring an entirely new array to be crated and returned.