# JML Tutorial - Exercises - Arithmetic

## 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