Multiple Method Behavior Exercises:

Multiple Method Behavior Tutorial

Question 1

Write the strongest specification for the code below that is needed to verify the method below? (Do not change the code, only write a specification.)

    public int mean(int sum, int totalNum) {
        if(totalNum == 0) {
            throw new ArithmeticException();
        }
        return sum/totalNum;  // ERROR: possible overflow!
    }

(The possible overflow would happen when sum is Integer.MIN_VALUE and totalNum is -1, since there is no positive equivalent to Integer.MIN_VALUE in the type int.)

Question 2

Consider the following class. Without changing the code, write a specification for the method max with multiple specification cases so that the method testMax verifies. (Do not change any of the code of either method.)

// openjml --esc IntMax.java
public class IntMax {
    //@ spec_pure
    public static int max(int x, int y) {
        if (y <= x) {
            return x;
        } else {
            return y;
        }
    }

    public static void testMax() {
        int m1 = max(5, 7);
        //@ assert m1 == 7;   // ERROR: may fail!
        int m2 = max(9, 7);
        //@ assert m2 == 9;   // ERROR: may fail!
        int m3 = max(11,11);
        //@ assert m3 == 11;   // ERROR: may fail!
    }
}

Learning Objectives:

  • Gain more experience identifying multiple method behaviors
  • Understand how to use the also clause
  • Understand the difference between normal_behavior and exceptional_behavior

Answer Key

Resources: