JML Tutorial - Exercises - Postconditions

Postcondition Exercises:

Postconditions Tutorial

Question 1

(a) Suppose that the function below had its specifications changed for num, where num is updated so that it only has to be greater than -1. Determine why this would cause an error, and how you could fix the remaining specifications to verify the function.

//@ requires 0 < num < 100;
//@ ensures \result > num;
 public int multiplyByTwo(int num) {
	return num*2;
}

(b) Suppose we revert to the orignal specifications where num > 0. The function is unable to be verified. Determine where in the specifications it is failing, and fix it.

(c) Suppose the code was updated to the following, and num must be a positive number. Determine the specifications needed to verify the function.

 public int multiplyByTwo(int num) {
	return num/2;
}

On the subject of “strongest” specifications: First let’s discuss what a strong predicate is. For the formula P implies Q, in this situation P is the strong preciate and Q is the weaker one. So when we say “strongest predicate” we are talking about the predicate that implies the other. For example, let’s think about the predicate that x > 1 implies x > 0, in this case the first predicate implies that x will always be greater than 5 which is greater than 0 - therefore it is true.

Therefore, when asking for the “strongest” specifications we want a strong precondition that implies the postcondition. One way to determine the stronger predicates is to find the specific inputs and outputs we want.. This allows for fewer implementations.

To read more about the subject check out the following

Learning Objectives:

Introduction to “strongest” specification
Understand overflow errors
Understand relationship between pre and post conditions

Question 2

Given a rectangle of width w and height h, write a function that finds the area of the rectangle and returns it. Determine the strongest specifications needed to verify the function. The function header is given below.

public int area(int w, int h);