Postcondition Exercises:

Postconditions Tutorial

Question 1

(a) Suppose that we want to change the precondition of the method multiplyByTwo below so that the argument (num) only has to be (strictly) greater than -1, that is the precondition would be `-1 < num < 100. Why would this cause a verification error with the existing code?

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

(b) How you could fix the postcondition so that the existing code would verify with the precondition -1 < num < 100? Note that you are to only change the postcondition, not the code in the body of the method and you are to use the new precondition -1 < num < 100.

Question 2

Consider the following code was updated to the following. What is the strongest postcondition that will allow the code in the body to be verified?

//@ requires 0 < num;
public int divideByTwo(int num) {
       return num/2;
}

Question 3

Given a rectangle of width w and height h: (a) write a Java method that finds the area of the rectangle and returns it. (b) What is the strongest specifications that verifies the code you wrote? The function header is given below.

public int area(int w, int h);

Question 4

Specify and correctly implement a method that returns the average of two doubles. The interface of the method should be as follows.

    public double average(double x, double y);

Learning Objectives:

  • Gain more experience writhing pre and postconditions
  • Understand the importance of postconditions and how they can be used to get the correct output for a program

Answer Key

All exercises