## Using Method Calls in Specifications Exercises Key:

### Question 1

(a) The program given below is unable to be verified; determine where in the specifications it is failing, and explain why it’s failing.

``````public class CallingMethodsExample2 {

//@ spec_public
final private double FAILINGGRADE = 69.4;
//@ spec_public
private int totalFailing = 0;
public boolean flag;

//@ assigns totalFailing;
//int count = 0;
for(int i = 0; i < grades.length; i++) {
//@ assume 0 <= i < grades.length;
//@ assume 0 <= totalFailing+1 < Integer.MAX_VALUE;
totalFailing++;
}
}
}
//@ assigns flag;

if((((double)totalFailing) / ((double)classSize)) >= .5){
flag = true;
return flag;
}else {
flag = false;
return flag;
}
}

public void testClass() {
double[] classGrades = {71.6, 31.5, 69.5, 69.3, 98.2, 84.3, 102.0};

}
}
``````

Asnwer and Explanation: Let’s break down what the code above is doing. First, we have three global variables `FAILINGGRADE`, `totalFailing`, and `flag`. The function `totalFailing()` increments the variable `totalFailing` by one every time it finds a grade, from the array `grades[]` passed in, that is less than or equal to `FAILINGGRADE`. Then, the function `isClassFailing()` takes in the class grades array and finds the length, then it will return true if over half the class is failing, and false otherwise. The function `testClass()` calls both these functions and then there is an assert statement that asserts the outcome of `isClassFailing()`. However, OpenJML throws an error when the program above is ran.

This is because `totalFailing()` is assigning the global variable `totalFailing` and therefore the function is not `pure` and cannot be used for JML specifications. For a function to be called in a specification it must be `pure`.

(b) Edit the code so that the original specifications verify the program.

Asnwer and Explanation: To verify the program with the original specifications would simply involve getting rid of the `assigns` statements. But to remove the `assigns` statement we need to remove the global variables `totalFailing` and `flag`, as well as the return type of `totalFailing()`. If we create and initialize `total` within the `isClassFailing()` function the assert statement should run without throwing an error. So we could write the following:

``````public class CallingMethodsExample1 {

//@ spec_public
final private double FAILINGGRADE = 69.4;

//@ pure
int count = 0;
for(int i = 0; i < grades.length; i++) {
//@ assume 0 <= i < grades.length;
//@ assume 0 <= count+1 < Integer.MAX_VALUE;
count++;
}
}
return count;
}

//@ pure

if((((double)total) / ((double)classSize)) >= .5){
return true;
}else {
return false;
}
}

public void testClass() {
double[] classGrades = {71.6, 31.5, 69.5, 69.3, 98.2, 84.3, 102.0};

}
}
``````

Note how the functions can now be `pure` since they are not modifying any memory locations. Additionally, note that the following are also valid ways of editing the code: (1) making `flag` a local variable of `isClassFailing()` (as it is not used elsewhere in the class), (2) rewriting the code to not assign to `flag` (3) rewriting the code to return the value of the if-statement’s test directly, as follows:

``````public /*@ pure @*/ boolean isClassFailing(double[] grades) {
return (((double)totalFailing) / grades.length) >= 0.5;
}
``````

Learning Objective: The goal of this exercise is to show the student why certain methods cannot be called in specifications when they are modifying memory. Students should recognize that method’s specifications are used to determine it’s behavior, not it’s implementation. Part (a) checks if the student can find why the function isn’t verifying, and part (b) asks the student to fix the code so that it does verify with the original specification which requires that they recognize that the error has to do with the `assigns` statements.