CSC/ECE 517 Fall 2009/wiki3 sskm

Programming By Assertions

Programming by assertion is method in which formal constraints are placed on the system's behavior which should always hold whenever the system is in a stable condition. The main goal of the assertions is to enforce what the system is supposed to rather than how to do it. In terms of any programming language, an invariant enables us to test the assumptions about our programs.

An example could be that in a 'stack' program, one assertion which should always hold true can be that the maximum number of elements at any point in the stack should never be more than the 'top' of the stack. Another example could be a method which calculates speed of any subatomic particle, can have an assertion enforced which says that the speed should always be less than the speed of light.

An assertion is composed of boolean expressions which are to be enforced. If the expression is true then we say that the assertion holds. If the boolean value is false then we say that the assertion does not hold and thus we have caught an 'error' which leads us to the next step of finding out and eliminating the bug. Thus programming by assertions is one of the quickest and most effective ways to detect and correct bugs because testing and debugging can sometimes be very tedious tasks to perform.

Structure of an assertion:

<assertion_type>(<condition>, <message>); where where <assertion_type> indicates what is the assertion made, <condition> indicates a boolean expression that helps to determine whether the assertion is violated or not; <message> will display an error information when the assertion is violated.

There are several classes of assertions which we will see next:

Preconditions, Postconditions, and Class Invariants

• Preconditions: These are assertions which must hold whenever a method is invoked. We will first see an example then will discuss whether using assertions explicitly here is advisable or not.

/**
* Sets the speed
*/
public void setSpeed(int speed) {
   // Enforce specified precondition in public method
   if (speed <= 0 || speed > MAX_SPEED)
       throw new IllegalArgumentException("Illegal speed: " + speed);
   setSpeedInterval(100/speed);
}

The example is self explanatory. Here the assertion/precondition on the input parameter is that the input speed can not be less than zero or more than the maximum speed. It is not advisable to use assert here. The reason is that the execution of the method (the Exception) guarantees that the precondition will always be enforced because of the exception that is thrown. So we do not need the assertion in this case of a public method. The use of an assertion will be redundant and sometimes should be avoided since the user is supposed to check the conditions which should hold for true program state, which the user is able to since it is a public method.

On the other hand, it is advisable to use assertions for methods which are not public because the code is not visible to the users so they can not code in their checks. In these cases assertions should be used as they help to preserve the correct program state.

• Postconditions: These assertions should hold after the execution of a method. A very naive or trivial example could be a function which squares of numbers of any sign (positive or negative) can have a postcondition which asserts that the result should be a positive real number.

public float Square(float m) {

       float result = m*m;
       assert (result >= 0) ;
       return result;
   }

Loop Invariants

A loop invariant is a relation among program variables that would be true when control enters a loop, remains true each time the program executes the body of the loop, and would still hold true when when the control exits the control exits the loop. Loop invariants can help us analyse the programs, check for errors(and derive programs from specifications)