Invariant checking

Back to Programming techniques

In programming, an invariant is a condition that must hold everytime the program executes through a specific position. This section offers ways to establish and check program invariants.

Theory

To analyze the correctness of a program, it is useful to split it into small blocks of functionality, where each block promises to do something, described by a set of postconditions, provided that its input fulfills certain preconditions. Most often, these blocks correspond to functions. Then the preconditions are a set of requirements for the arguments that are passed in, and the postconditions are a set of effects that the function results in. However, more fine grained checking inside a function is appropriate when the algorithm is complex. While preconditions concern checking the arguments that the user of the function passed in, those invariants internal to a function concerns the correctness of the implementation.

Practice

Pastel provides the macros ENSURE, PENSURE, and ASSERT, to help with enforcing invariants. All of the three macros work in exactly the same way, so we will demonstrate their functionality by taking ENSURE as an example. The following demonstrates the use of ENSURE in an actual situation.

SubMatrix& operator=(const SubMatrix& that)
{
    ENSURE2(width_ == that.width_,
        width_, that.width_);
    ENSURE2(height_ == that.height_,
        height_, that.height_);
    //...
}    

ENSURE takes in a condition that must hold for the program to continue execution beyond that point. The number 2 denotes that in the case the condition is not satisfied, we want to report the values of two variables that are listed after the condition. Corresponding to the number of reported parameters, there are also ENSURE, ENSURE1, ENSURE2, ENSURE3, and ENSURE4.

In our example, the precondition is that the SubMatrix’s must have equal width and height when one is assigned into another. In case that the conditions are satisfied, the program continues to execute the rest of the function. But if the conditions are not satisfied, then the following happens:

  1. The violated condition, file name, function name, line number, and the parameters are printed into a log.
  2. The program takes an invariant failure action.

Triggering an ENSURE means that there is a bug at the user’s side (or a bug at the condition itself). Triggering an ASSERT means that there is a bug in the implementation side of the algorithm (or a bug at the condition itself). The user can choose the taken action on an invariant failure. Choices include calling std::abort(), throwing an exception, or either of these with a preceding assert() (to invoke a possible debugger when in debug mode).

The case of the binary operator

For the common case of testing two integer or floating point variables with a binary operator, Pastel implements ENSURE_OP, PENSURE_OP, and ASSERT_OP macros. They allow to avoid the redundant duplication of the testing parameters:

SubMatrix& operator=(const SubMatrix& that)
{
    ENSURE_OP(width_, ==, that.width_);
    ENSURE_OP(height_, ==, that.height_);
    //...
}    

Performance

There is a problem with very short functions where the invariant checking can induce a relatively big performance degradation (for example, in checking the index bounds when accessing an array). To solve this problem, Pastel offers the macro PENSURE, which stands for “Performance ENSURE”. This macro is automatically removed from release versions by conditional compilation. It is intended to be used only in those rare situations where the cost of invariant checking is relatively too big. As a rule of thumb, I use PENSURE for functions that are of order or less, and ENSURE for all others.

Conditional compilation

ENSURE‘s are always present in the program and can’t be removed by conditional compilation from the program. This is to stress the point that precondition checking is always important, also in release versions. This is because in the case that a bug occurs, it is important to know about it.

The ASSERTs and PENSUREs are present if and only if DEBUG or _DEBUG is defined in the preprocessor.

Justification for the use of a macro

The reason for using macros, which are well known for their disadvantages, is to be able to report the file name, the function, the line number, and the condition. Only the preprocessor can do this, and thus the use of a macro is necessary.

Files

Invariant checking

Contains ENSURE, PENSURE, and ASSERT macros.