Arithmetic Exercises:

Arithmetic and Arithmetic Modes Tutorial

Question 1

Given the method below determine the strongest preconditions needed to verify it.

// openjml --esc ArithmeticExample1.java
public class ArithmeticExample1 {
	
    private int sum;

    public void sumThreeNums(int n1, int n2, int n3) {
        sum = n1 + n2 + n3;   // ERROR: may overflow!
	//@ assert 0 <= sum <= Integer.MAX_VALUE;   // ERROR: may fail!
    }
	
}

Learning Objectives:

  • Understand overflow and underflow errors and how to use specifications to prevent them.

Question 2

(a) The method given below cannot be verified; write an assume statement (or several assume statements) in the code, without changing the Java code, to allow it to be verified.

(b) How could you edit the code to allow the method to verify without adding any specifications?

// openjml --esc ArithmeticExample2.java
public class ArithmeticExample2 {
    private int playerHealth;
	
    public int updatePlayerHealth(int dmg) {
        playerHealth -= dmg;   // ERROR: may underflow or overflow!
        if (playerHealth < 0) {
            playerHealth = 0;
        }
        return playerHealth;
    }
}

Learning Objectives:

  • Gain more experience with handling overflow
  • Understand how to write specifications that reflect the requirements and outputs wanted

Answer Key

Resources: