Pre and Postconditions

Objective #1: Interpret preconditions and postconditions.

• A precondition is something that a client programmer guarantees to a method. Usually a precondition is a statement about the parameters of the method that is guaranteed to be true.
  
  
• For example, in the following method
  
  public double divide(double num1, double num2)
  {
     return num1 / num2;
  }
  
  an appropriate precondition would be to guarantee that num2 does not equal zero. Otherwise, the code would "crash" with a run-time error.
  
  
• On the AP exam, the preconditions are typed into a javadoc comment that appears immediately above the method.
  
  /**
   * Precondition: num2 is not zero.
   */
  public double divide(double num1, double num2)
  {
     return num1 / num2;
  }
  
  
• It is the responsibility of the client programmer to be sure that he/she does not pass parameters that violate a method's precondition. If a precondition is violated when a method executes, a good class developer will throw an exception from the method. An exception is an object that indicates that an error occurred. A client program can be designed to catch exceptions in order to run more effectively. We will study exceptions in more detail later in this course.
  
  
• A postcondition is something that the method guarantees to the client programmer that will happen as a result of calling the method. Postconditions are sometimes typed into javadoc comments on the AP exam as well.
  
  /**
   * Precondition: num2 is not zero.
   * Postcondition: Returns the quotient of num1 and num2.
   */
  public double divide(double num1, double num2)
  {
     return num1 / num2;
  }
  
  
• For example, the following version of the method does not have the requirement that num2 is not zero. Instead it uses an if statement to avoid a run-time error if num2 is zero. Compare its pre and post-conditions to the earlier example of the method.
  
  /**
     precondition: none
     postcondition: Returns the quotient of num1 & num2. If num2 is zero, zero is returned.
  */
  public double divide(double num1, double num2)
  {
  
     if (num2 != 0)
     {
        return num1 / num2;
     }
  
     return 0;
  }
  
  
• In the free response section of the AP exam, the exam writer will provide the postcondition within the methods that have to be written. Be sure to read the postcondition carefully and make sure that you satisfy every part of it. Postconditions can be very complicated.
  
  
• It is good style to type a full javadoc comment that includes descriptions about the parameters, return values, etc. See the wikipedia entry at http://en.wikipedia.org/wiki/Javadoc for more info. The @param and @return tags are standard javadoc notations that make it easier for a programmer to automatically create an API as a set of HTML web pages. The @param tag is used to explain the purpose of each parameter. The @return tag is used to explain what is being returned by a method and is essentially the postcondition. Normally pre and postcondition information is worded into the @param and @return tags instead of being found on lines of their own like you'll see it on the AP exam.
  
  Here is a full example
  
  /**
   * Divides two numbers.
   * Precondition: num2 is not zero.
   * Postcondition: Returns the quotient of num1 and num2.
   * @param num1 the numerator
   * @param num2 the denominator
   * @return the quotient of num1 and num2
   */
  public double divide(double num1, double num2)
  {
     return num1 / num2;
  }

Objective #2: Identify class invariants.

• A class invariant is an expression that is always true about an object variable of the class at any point while a client program executes. For example, you might have a class named Student in which there is an instance field named myGPA. Because of the following constructors and modifier method, there would be no possible way for myGPA to ever become a negative number. So a class invariant for the Student class would be "A student has a positive GPA".
  
  public Student()
  {
     myGPA = 0;
  }
  
  public Student(double gpa)
  {
     if (gpa >= 0)
     {
        myGPA = gpa;
     }
     else
     {
        myGPA = 0;
     }
  }
  
  public void setGPA(double gpa)
  {
     if (gpa >= 0)
     {
        myGPA = gpa;
     }
     else
     {
        myGPA = 0;
     }
  }