Arithmetic Exercises:

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;

Learning Objectives:

  • Understand overflow and underflow errors
  • Understand Integer.MAX_VALUE
  • Gain more experience writing preconditions
  • Gain 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. (b) How could you edit the code to verify the function with the original specification?

//@ 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 Objectives:

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

Answer Key

All exercises