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:

Internal Invariants

These assertions were used before the programming languages had the support of an explicit assert keyword. Internal logic and program's language constructs were used to assert the assertions in the program's native.

For example before assert keyword, we would use this code:

if (i % 3 == 0) {
       ...
   } else if (i % 3 == 1) {
       ...
   } else { // We know (i % 3 == 2)
       ...
   }

The same code with the use of assert keyword can be written as:

if (i % 3 == 0) {
       ...
   } else if (i % 3 == 1) {
       ...
   } else {
       assert i % 3 == 2 : i;
       ...
   }

Preconditions, Postconditions, and Class Invariants

Before moving on to explain it, it is worth mentioning that even though the assert construct is not a full-blown design-by-contract method of programming, it helps to support an informal design-by-contract style of programming.

• 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.

For example

/**
* 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 private 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. (Assert is for private arguments only)

• 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;
   }

• Class Invariants: Class invariant is the property of the state of the class which should hold at all times for all instances of the class(objects in other words), except when the class in a transition state. In other words it defines all valid states for an object and ensures the correct working of a class. The class invariants should hold before and after the execution of any method. So in simpler words class invariants are used to put constraints on objects and the methods of the class should preserve it at all times (not necessarily while method execution but before and after it).

Class invariants must hold when an object is created, and they must be preserved under all operations of the class. In particular all class invariants are both preconditions and post-conditions for all operations or member functions of the class.

Jass is a extension tool of Java with Assertions in which class invariants can be specified using the keyword invariant.

public class Buffer {
...
/** invariant 0 <= count && count <= capacity(); **/
}

Advantages & disadvantages of assertions

1. Assertions aren't generally used in production code because there is an overhead and it is assumed that situations where the invariants fail have been caught as coding errors during development and testing. Moreover we can't replace exception handling with assertions because if the user runs the application with assertions disabled (the default), all of the error handling code disappears

2. When to use assertions, when to use exceptions ? :

Assertions are for ensuring that the Contract is being adhered to. The contract must be fair, so that client must be in a position to ensure it complies. For example, you can state in a contract that a URL must be valid because the rules about what is and isn't a valid URL are known and consistent.

Exceptions are for situations that are outside the control of both the client and the server. An exception means that something has gone wrong, and there's nothing that could have been done to avoid it. For example, network connectivity is outside the applications control so there is nothing that can be done to avoid a network error.

In other words, assertions are for programmers to tell, something went wrong. Exceptions are for end users to know something gone wrong.

3. Another observation is that the preconditions are typically (though not always) cheaper to test than invariants and postconditions, and that in some cases correctness and "safety" in the release build are more important than speed. i.e. For many applications speed is not an issue, but robustness (the ability of the program to behave in a safe way when its behaviour is not correct, i.e. when a contract is broken) is.

If you're making software for a bank, it might be better to interrupt execution with an alarming message than to transfer $1,000,000 instead of $1,000. But what if you're programming a game? Maybe you need all the speed you can get and if someone gets 1000 points instead of 10 because of a bug that the preconditions didn't catch (because they're not enabled), tough luck.

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)

Example 1 for Loop Invariant:

Consider the following example in which the Java method namely sum takes an integer array a as an argument and returns the sum of elements of array a. s is local variable that contains the sum of the elements and integer i is used to index the elements in the array.

public static int sum(int a[])
{
    int s = 0;
    for (int i = 0; i < a.length; i++)
    {
        // s is the sum of the first i array elements
        // s == a[0] + .. + a[i-1]
        s = s + a[i];
    }
    return s;
}

The comments in the loop body describe the invariant. The first comment describes the invariant that s is the sum of the first i array elements. The second comment expresses the invariant that the sum s is given by s == a[0] + .. + a[i-1]. This emphasizes that the invariant is an assertion, an expression that should always evaluate to true.

The invariant expresses a relation between the three variables s, i, and a that remains true even when the values of s and i change: s is always the sum of the first i elements in a. When control enters the loop, i is 0 so s is the sum of no array elements. When control exits the loop, i is a.length, so s is the sum of all of the array elements. This is the intended result.

The above example shows the way in which loop invariants can help us in writing programs. When the program exits a loop, the loop invariant expresses the intended values of the variables at that point. Therefore we can work backwards from the intended values to the loop invariant, and then to the code itself. This can be a systematic method for writing programs which can supplement the usual method of relying on intuition and lots of trial-and-error.

Example 2: Consider the following algorithm on Bubble sort

Algorithm Bubblesort(sequence):

Input: sequence of integers sequence
Post-condition: sequence is sorted & contains the same integers as the original sequence

length = length of sequence
for i = 0 to length - 1 do
  for j = 0 to length - i -2 do
    if jth element of sequence >(j+1)th element of sequence
    then
        swap jth and (j+1)th element of sequence

In the above example, we have two loop invariants. One for the outer loop and one for the inner loop. Loop Invariant for Outer Loop: Last i elements of sequence are sorted and are all greater or equal to the other elements of the sequence.
Loop Invariant for inner Loop: Same as outer loop and the jth element of sequence is greater or equal to the first j elements of sequence.