1.9 Preconditions and Postconditions

When defining the operations of an ADT, we must include a specification of required inputs and the resulting output, if any. In addition, we must specify the preconditions and postconditions for each operation. A precondition indicates the condition or state of the ADT instance and inputs before the operation can be performed. A postcondition indicates the result or ending state of the ADT instance after the operation is performed. The precondition is assumed to be true while the postcondition is a guarantee as long as the preconditions are met. Attempting to perform an operation in which the precondition is not satisfied should be flagged as an error.

Consider the use of the pop(i) method for removing a value from a list.

When this method is called, the precondition states the supplied index must be within the legal range. Upon successful completion of the operation, the postcondition guarantees the item has been removed from the list. If an invalid index, one that is out of the legal range, is passed to the pop method, an exception is raised.

Now, consider the following code segment

which results in an "Index out of range" exception

   Traceback (most recent call last):
     File "<stdin>", line 1, in <module>
   IndexError: pop index out of range

because we are trying to pop an element beyond the end of the list.

All operations have at least one precondition, which is that the ADT instance has to have been previously initialized. In an object-oriented language, this precondition is automatically verified since an object must be created and initialized via the constructor before any operation can be used. Other than the initialization requirement, some operations may not have any other preconditions. It all depends on the type of ADT and the respective operation. Likewise, some operations may not have a postcondition, as is the case for simple access methods, which simply return a value without modifying the ADT instance itself.

Throughout the text, we do not explicitly state the precondition and postcondition as such, but they are easily identified from the description of the ADT operations. For example, the definition of the slope operation for the Line Segment ADT indicates "The line segment can not be vertical."

When implementing abstract data types, it is important that we ensure the proper execution of the various operations by verifying any stated preconditions. The appropriate mechanism when testing preconditions for abstract data types is to test the precondition and raise an exception when the precondition fails. You then allow the user of the ADT to decide how they wish to handle the error, either catch it or allow the program to abort.

Python, like many other object-oriented programming languages, raises an exception when an error occurs. An exception is an event that can be triggered and optionally handled during program execution. When an exception is raised indicating an error, the program can contain code to catch and gracefully handle the exception; otherwise, the program will abort.

Python also provides the assert statement, which can be used to raise an AssertionError exception. The assert statement is used to state what we assume to be true at a given point in the program. If the assertion fails, Python automatically raises an AssertionError and aborts the program, unless the exception is caught.

Returning to the implementation of the slope method for the LineSegment class, a correct solution must first test the precondition. This is done using the assert statement and specifying what we expect to be True, that the line is not vertical:

If the assertion fails, which will happen when the line is vertical, Python will raise an AssertionError. If the error is caught and handled, the program continues. Otherwise, the program aborts and an error message is displayed:

   Traceback (most recent call last):
     File "line.py", line 4, in <module>
   AssertionError: Line segment can not be vertical.

The last line of the error message includes the string provided as the second argument to the assert statement. The purpose of this string is to provide the programmer with information to aide in debugging the error. The first argument of the assert statement can be any logical expression or a function call that returns a Boolean value.

The new implementation of the slope method is provided below:

Throughout the text, we use the assert statement to test the preconditions when implementing abstract data types. This allows us to focus on the implementation of the AD Ts instead of having to spend time selecting the proper exception to raise or creating new exceptions for use with our AD Ts. For more information on exceptions and assertions, refer to AppendixC.

A new listing of our implementation of the LineSegment class is provided below with the new line highlighted. The implementation of several operations is left as an exercise.