## Verifying Method Calls Exercises Key:

### Question 1

Write two functions that perform the following: an function that adds two integer arrays and a function that returns true if the arrays to be added are of the same size. Use the following function headers to help you. Determine the specifications needed to verify your functions.

``````public int[] addArrays(int[] a, int[] b);

public boolean sameSize(int[] a, int[] b);
``````

Answer and Explanation: We are tasked with writing a program that adds two integer arrays, we will break up this process into two functions. The `addArrays()` will take in two integer arrays `a` and `b` and will add their elements if they are the same size. The `sameSize()` will also take in the arrays `a` and `b` and check if they have the same length. Given this information we can write something like the following program:

``````public int[] addArrays(int[] a, int[] b) {
if(sameSize(a, b)) {
int[] newArr = new int[a.length];
for(int i = 0; i < a.length; i++) {
newArr[i] = a[i] + b[i];
}
return newArr;
}
return new int[0];
}

public boolean sameSize(int[] a, int[] b) {
return a.length == b.length;
}
``````

The `addArrays()` function calls `sameSize()`, and if `a.length == b.length` a new integer array `newArr` is created of size `a.length`. Note, that it could also be of the size `b.length`, it doesn’t really matter since we have determined at this point they are the same size. After creating `newArr` there is a for-loop that runs for the length of `a` and will store `a[i] + b[i]` at `newArr[i]`. If `a` and `b` are NOT the same size the function will return an empty integer array which is written as `new int[0]`. The `sameSize()` function simply returns the result of checking if `a.length == b.length`, that is to say it will return true if `a` and `b` are the same length, and false otherwise.

Now that we have written the code, what preconditions and postconditions should be included? Well, first let’s write any JML specifications for `sameSize()` as it is a more straightforward function. For `sameSize()` we can ensure that the result will always be equivalent to whether `a.length == b.length` (i.e true or false). So we might write something like the following for `sameSize()`

``````public int[] addArrays(int[] a, int[] b) {
if(sameSize(a, b)) {
int[] newArr = new int[a.length];
for(int i = 0; i < a.length; i++) {
newArr[i] = a[i] + b[i];
}
return newArr;
}
return new int[0];
}
//@ ensures \result <==> (a.length == b.length);
public boolean sameSize(int[] a, int[] b) {
return a.length == b.length;
}

``````

As for the `addArrays()` function let’s think about what preconditions we might want to require; we are adding the elements from `a` and `b` and any time we are dealing with integer arithmetic we want to make sure we remain in the size of type `int`. So we can use the `forall` clause to check that `a[i] + b[i] <= Integer.MAX_VALUE`. Additionally, since the function will return an empty array if `a` and `b` aren’t the same size we can ensure two things to be true. The `\result` will have the length equal to that of either array `a` or `b`. Secondly, if `a` and `b` aren’t the same length then `\result` will be empty and have the length of zero.

Note: We can write more complex `ensures` clauses that would actually check if the function `addArrays()` returns an array whose elements are equal to that of `a[i] + b[i]`, but that would require the use of loop invariant which we will get into in the “Specifying Loops” tutorial. Additionally, as we move on you will see better ways of handling exceptions and different method behaviors, but for now we can write something like the following:

``````//@ requires (\forall int j; 0 <= j < a.length; a[j]+b[j] <= Integer.MAX_VALUE);
//@ ensures \result.length == a.length || \result.length == 0;
//@ pure
public int[] addArrays(int[] a, int[] b) {
if(sameSize(a, b)) {
int[] newArr = new int[a.length];
for(int i = 0; i < a.length; i++) {
newArr[i] = a[i] + b[i];
}
return newArr;
}
return new int[0];
}

//@ ensures \result <==> (a.length == b.length);
public boolean sameSize(int[] a, int[] b) {
return a.length == b.length;
}
``````

Now, since we are dealing with a for-loop we also have to include an assume statement so we don’t run into any issues going out-of-bounds. Additionally, since we’re adding `a[i] + b[i]` we need to account for potential overflow errors like we did in our precondition, so let’s also include an assume statement that handles this.

``````//@ requires (\forall int j; 0 <= j < a.length; a[j]+b[j] <= Integer.MAX_VALUE);
//@ ensures \result.length == a.length || \result.length == 0;
//@ pure
public int[] addArrays(int[] a, int[] b) {
if(sameSize(a, b)) {
int[] newArr = new int[a.length];
for(int i = 0; i < a.length; i++) {
//@ assume 0 <= i < a.length;
//@ assume Integer.MIN_VALUE < a[i] + b[i] <= Integer.MAX_VALUE;
newArr[i] = a[i] + b[i];
}
return newArr;
}
return new int[0];
}

//@ ensures \result <==> (a.length == b.length);
public boolean sameSize(int[] a, int[] b) {
return a.length == b.length;
}
``````

Now that we have included everything from past tutorials, what new specifications do we need after reading “Method Calls?” Recall how a method call is verified; at the call site the precondition of the called method is asserted, and then the callee’s postconditions are assumed. In our program we only have one preconditions for the caller function `addArrays()` which we’ve already accounted for, and one postcondition for the callee function `sameSize()`. So we can write the following:

``````//@ requires (\forall int j; 0 <= j < a.length; a[j]+b[j] <= Integer.MAX_VALUE);
//@ ensures \result.length == a.length || \result.length == 0;
//@ pure
public int[] addArrays(int[] a, int[] b) {
if(sameSize(a, b)) {
//@ assert sameSize(a, b);
int[] newArr = new int[a.length];
for(int i = 0; i < a.length; i++) {
//@ assume 0 <= i < a.length;
//@ assume Integer.MIN_VALUE < a[i] + b[i] <= Integer.MAX_VALUE;
newArr[i] = a[i] + b[i];
}
return newArr;
}
return new int[0];
}

//@ ensures \result <==> (a.length == b.length);
public boolean sameSize(int[] a, int[] b) {
return a.length == b.length;
}
``````

Learning Objective: The goal of this exercise is to see if the student understands how to verify method calls. This is a rather simple example, so the student should be able to identify the statements needed to verify functions. The exercise also checks that the student understands and can utilize information from past exercises as well. It also checks if the student can also identify all specifications needed - not just those used for verifying method calls.

### Question 2

The program below is checking whether the user has enough material for an area given the dimensions of the area and the amount of material the user has. However, the program is unable to be verified; determine where in the specifications it is failing, and fix it.

``````//@ ensures \result <==> (area(w, h) > materialSqFt);
public boolean enoughMaterial(int materialSqFt, int w, int h) {
int area = area(w, h);

return (area > materialSqFt);
}

//@ ensures \result > 0;
//@ ensures \result >= w;
//@ ensures \result >= h;
//@ pure
public int area(int w, int h) {
int A = w*h;

return A;
}
``````

Answer and Explanation: The program above is unable to be verified with its current specifications; let’s break it down and see where the issues lie. The first function `enoughMaterial()` takes in three integer variables `materialSqFt`, `w`, and `h`. It then creates an integer `area` which is set equal to the function `area(w,h)`. If we drop down to the `area()` function we see that the code is the same as we’ve seen in past exercises, and simply finds the rectangular area given `w` and `h` and returns it. After `area(w,h)` is called in `enoughMaterial()`, the function checks if the `area > materialSqFt`. In the event that `area > materialSqFt` it returns false, otherwise it returns true.

First, we can see that there will be an overflow error in the function `area()` unless we include a precondition that checks that `0 <= w <= Integer.MAX_VALUE` and `0 <= b <= Integer.MAX_VALUE`. Otherwise, all our preconditions and postconditions for the two functions look good.

However, since `enoughMaterial()` calls `area()` we need to include some `assume` and `assert` statements to verify the two methods. Again we know the process for any function is at the call site assert the precondition of the called method, and then assume the callee’s postconditions. So what might we include in the program above?

Let’s start in the function `area()`; after we include that `w` and `h` need to be greater than zero, and less than or equal `Integer.MAX_VALUE`, we would need to assume this in the function. We would also want to assume that `w*h <= Integer.MAX_VALUE` so we don’t get any overflow errors. After the body of the function and before the return statement, we want to include an `assert` statement that asserts our area postconditions. Now, back to the `enoughMaterial()` function, in this function we want to `assume` its preconditions, and `assert` its postconditions. However, before we call `area()` we want to assert `area()`’s precondtions, and then `assume` its postconditions after the call. So we can write something like this to verify the program:

``````//@ requires materialSqFt > 0;
//@ requires 0 < w <= Integer.MAX_VALUE & 0 < h <= Integer.MAX_VALUE;
//@ ensures \result <==> (area(w, h) > materialSqFt);
public boolean enoughMaterial(int materialSqFt, int w, int h) {
//@ assume materialSqFt > 0 && 0 < w <= Integer.MAX_VALUE & 0 < h <= Integer.MAX_VALUE;

//@ assert 0 < w <= Integer.MAX_VALUE && 0 < h <= Integer.MAX_VALUE;
int area = area(w, h);

//@ assume area > 0 && area >= w && area >= h;

//@ assert (area > materialSqFt);
return (area > materialSqFt);
}

//@ requires 0 < w <= Integer.MAX_VALUE & 0 < h <= Integer.MAX_VALUE;
//@ ensures \result > 0;
//@ ensures \result >= w;
//@ ensures \result >= h;
//@ pure
public int area(int w, int h) {
//@ assume 0 < w <= Integer.MAX_VALUE & 0 < h <= Integer.MAX_VALUE;
//@ assume w*h <= Integer.MAX_VALUE;
int A = w*h;

//@ assert A > 0 && A >= w && A >= h;
return A;
}
``````

Learning Objective: The goal of this exercise is to show the student the necessity of verifying method calls. This exercise is much more complex than the first exercise, and shows that the program cannot be verified without out `assume` and `assert` statements of the pre and postconditions. We want the student to get more comfortable with the process of verifying method calls, and understand it follows the same process every time.