Arithmetic Exercises Key:

Arithmetic Tutorial

Question 1

Given the function below determine the strongest preconditions needed to verify the function.

public class ArithmeticExample1 {
	//@ spec_public
	private int sum;

	//@ ensures 0 < sum < Integer.MAX_VALUE;
	public void sumThreeNums(int n1, int n2, int n3) {
		sum = n1 + n2 + n3;
	}	
}

Asnwer and Explanation: First let’s break down the code. The function sumThreeNums() takes in three integer variables n1, n2, and n3 and will add them together and set the global variable sum equal to the result. We are given our postoncdition of the function which states that sum must be greater than zero and less than Integer.MAX_VALUE. Integer.MAX_VALUE is simply a variable of the class Integer that is the largest possible value of type int. If we were to run this code using OpenJML we would get many warnings concerning the Arithmetic Operation Range. What this means is essentially OpenJML cannot verify that the function will not have any overflow or underflow errors when it passes in all possible inputs. So we need to tell OpenJML what our range of n1, n2, and n3 can be.

Given the postcondition that sum must be less than Integer.MAX_VALUE we can determine that all of our integers passed in must also be less than Integer.MAX_VALUE otherwise one variable on it’s own will cause an overflow error because it could be greater than the largest value of type int. Additionally, we are told that sum must be greater than zero, so we also need to reflect this in our requirements for out integer variables passed in. As such, we can write something like the following:

public class ArithmeticExample1 {
	//@ spec_public
	private int sum;

	//@ requires 0 < n1 < Integer.MAX_VALUE;
	//@ requires 0 < n2 < Integer.MAX_VALUE;
	//@ requires 0 < n3 < Integer.MAX_VALUE;
	//@ ensures 0 < sum < Integer.MAX_VALUE;
	public void sumThreeNums(int n1, int n2, int n3){
		sum = n1 + n2 + n3;
	}	
}

While we might think we are done, we are not. OpenJML still cannot verify tht adding all of these numbers together won’t cause and overflow or underflow error so let’s take care of that. Let’s take a look at what sum is equal to in our function. In our function sum = n1 + n2 + n3, therefore, we need to make sure that n1 + n2 + n3 is less than Integer.MAX_VALUE. We might say (n1 + n2 + n3) < Integer.MAX_VALUE but this on its own isn’t really doing anything we haven’t said. Let’s rework it to be n1 < Integer.MAX_VALUE/(n2 + n3) which we know is valid because of Alegrba. However, now OpenJML cannot verify that n2 + n3 isn’t greater than or equal to Integer.MAX_VALUE so we need to check that n2 < Integer.MAX_VALUE/n3. Note, we don’t have to worry about dividing by zero since we explicitly stated that our numbers are greater than zero - if we didn’t do this it would cause warnings of possible divisions by zero.

Also, note that we are modifying the memory of global variable sum and should therefore specify this in our speicifations. That being said, let’s write the following:

public class ArithmeticExample1 {
	//@ spec_public
	private int sum;

	//@ requires 0 < n1 < Integer.MAX_VALUE;
	//@ requires 0 < n2 < Integer.MAX_VALUE;
	//@ requires 0 < n3 < Integer.MAX_VALUE;
	//@ requires n2 < Integer.MAX_VALUE/n3;
	//@ requires n1 < Integer.MAX_VALUE/(n2 + n3);
	//@ assigns sum;
	//@ ensures 0 < sum < Integer.MAX_VALUE;
	public void sumThreeNums(int n1, int n2, int n3){
		sum = n1 + n2 + n3;
	}	
}

Learning Objective: The goal of this exercise is to make the student more comfortable with handling potential overflow and underflow errors. We want the student to be aware the while the compiler will not throw any errors about overflow/underflow errors, OpenJML will test all possible inputs and therefore if the student doesn’t specify the range of their variables it won’t verify. We also introduce the student to Integer.MAX_VALUE and ask them to think critically about the steps needed to verify the function. The student should recongize that in order for n1 + n2 + n3 to be less than Integer.MAX_VALUE we need to make sure that n2 + n3 is less than Integer.MAX_VALUE. This exercise also gives the student more experience with the assigns clause.

Question 2

(a) The function given below is unable to be verified; determine where in the specifications it is failing, and fix it.

//@ spec_public
	private int playerHealth;
	
	//@ requires dmg <= 0;
	//@ requires 0 < playerHealth;
	public int updatePlayerHealth(int dmg) {
		if(playerHealth > dmg) {
			return (playerHealth - dmg);
		}else {
			return 0;
		}
	}

Asnwer and Explanation: First let’s assess what the current preconditions are requiring of both playerHealth and dmg. The first precondition requires that dmg be a negative number. Next, the program requires that playerHealth be greater than or equal to zero. Now, within the function we check if playerHealth is greater than dmg, and if it is we return playerHealth - dmg, otherwise we return zero - since the player would be dead if their health is less than the dmg attack or zero.

Can you determine the error in the preconditions given the code? Notice how we require that dmg be negative but we return playerHealth - dmg, which would mean we are actually returning playerHealth - (-dmg) = playerHealth + dmg (since dmg has to be negative). This would cause an error since we would now potentially have an overflow error since we are adding dmg to playerHealth and playerHealth is not bounded with Integer.MAX_VALUE. To fix this we need to require that dmg be a positive number since it is we are subtracting dmg from playerHealth. So we write the following:

//@ spec_public
private int playerHealth;
	
//@ requires 0 <= dmg < Integer.MAX_VALUE;
//@ requires 0 < playerHealth;
public int updatePlayerHealth(int dmg) {
	if(playerHealth > dmg) {
		return (playerHealth - dmg);
	}else {
		return 0;
	}
}

(b) How could you edit the code to verify the function with the original specification?

Asnwer and Explanation: To keep the original preconditions without errors we would have to make a small edit to the code. The original problem with the function was that playerHealth - (-dmg) = playerHealth + dmg. So if we want to require that dmg be negative we need to change the return to playerHealth + dmg so that playerHealth + (-dmg) = playerHealth - dmg. So we can write the following:

 //@ spec_public
private int playerHealth;
	
// @ requires dmg <= 0;
//@ requires 0 < playerHealth;
public int updatePlayerHealth(int dmg) {
	if(playerHealth > dmg) {
		return (playerHealth + dmg);
	}else {
		return 0;
	}
}

Learning Objective: The goal of this exercise is to see if the student understands how they need to account for OpenJML testing all possible inputs that conform to the preconditions. While the exercises focuses on using the correct opteration we want to show the student how not using the correct operation would cause error. Given the preconditions and the code in part (a) the student needs to recognize that since OpenJML will test negative values for dmg it will cause overflow warnings because with the code it returns playerHealth + dmg. Additionally, in part (b) we want to see if the student understands how the original precondition can still be used to have the same result if the code makes sense with the input OpenJML passes in. At this point in the students studies they have seen numerous examples of potential overflow errors and how to handle them, so this should be an easier exercise.

Resources: