Home Up Intro Contents Chapter 1 2 3 4 5 6 7 8 9 10 Design Assert Timing EBNF Report Pas Last Changed: Nov. 19, 1997
This is a conversion from Oberon text to HTML. The converter software is still under development, and some features or information may be missing in this converted version. HTML hypertext facilities are not yet active in this document. To exploit the interactive facilities, use Oberon System 3 and the source of this text, available as ASCII-coded Oberon System 3 documents. A previous version is also available for Oberon V4. To access this and other additional material use ftp.
For the convenience of our students, most of this information and the related material is in German. Sorry if this is not one of your languages.

Einführung in die Programmiersprache Oberon.

G. Sawitzki <gs@statlab.uni-heidelberg.de>

12 Assertions, Tests, Invariants
-- This chapter should be accompanied by a proper case study.
A recommended case study is Mess.Mod,
accessible at statlab.uni-heidelberg.de --

This chapter deals with one special language construct, assertions, and a very special interpretation of this construct.
Formally, assertions are supported by a predeclared procedure which may come in one of two forms
  ASSERT(x, n) x: Boolean expression; n: integer constant
    terminate program execution if not x
  ASSERT(x)  x: Boolean expression
    terminate program execution if not x
The first form is roughly equivalent to the statement
The second form uses a system defined termination code, instead of the user defined value n. The difference between HALT and ASSERT is that ASSERT may be handled in two different ways by compilers or systems: In most systems, a loader or compiler option is provided to enable/disable code generation for ASSERT procedures. If ASSERT is switched off, ASSERT calls will be ignored and no code is generated for them.

The special interpretation we give to this construct is to view ASSERT as a means to specify necessary conditions for the correctness of a program. With this interpretation, ASSERT is a means to integrate aspects of the program specification in program code, allowing at least partial verification.

With this interpretation in mind, compiler options to switch ASSERTs on/off should be handled with care. If it can be guaranteed that the boolean control condition is always true, a compiler is free and welcome to suppress code generation for an ASSERT statement, as it is for the comparable HALT statement if in a "dead" branch. (Dead code removal, i.e. suppression of code which cannot be reached, is a common compiler technique, and no special construct is needed for this.) If, on the other hand, the ASSERT condition cannot be guaranteed, the alternative cannot be excluded and will be encountered if a necessary condition for successful program execution is not satisfied. An exception should be taken, and if it is not provided by reasonable program code, a HALT is a proper bail out. So the recommendation is: do not use ASSERT as "debugging statement" which is switched off in production code:
  Never disable ASSERT.

On the other hand, an ASSERT call is an invitation to the compiler for closer inspection whether the ASSERT code can be omitted. That is the compiler is challenged to prove that the ASSERT condition is always guaranteed. Unfortunately, the evaluation of the boolean expression x may have side effects. For example, the evaluation may imply the evaluation and possible change of some state variable, which may affect other parts of the program execution. This is allowed, but makes program verification and automatic dead code removal difficult. So the second recommendation is: Don't allow side effects.
  No side effects in ASSERT conditions.

Both rules are recommendations, no obligations. They reflect our special interpretation of ASSERT.

ASSERT may be used in several typical roles. We go through the most typical ones.

Environmental conditions
Environmental conditions specify requirements on the computing environment. For example, to use LONGINT based integer numbers, you may want to check that you have at least 32-bit LONGINTs. Using
in the module initialization part, where "100" is an ad hoc error code, may be a convenient check. Most compilers will handle this ASSERT already during compilation. Either the constant value of SIZE(LONGINT) is guaranteed to exceed 4, and no code for the ASSERT will be generated, or SIZE(LONGINT)<4, and the compiler will issue an error message and possibly abort compilation. This however may affect the portability of a program. Asserts checked at compilation time reflect the compilation environment. If the run time environment does not coincide with the compilation environment, problems may occur.

Preconditions test for the legal input to procedures. Usual application preconditions require parameters to be in certain ranges. For example, to time a procedure, you may use a timing routine
  PROCEDURE TimeIt(proctotime:PROCEDURE; runs:INTEGER)
with a precondition expressed as
where "100" is again an ad hoc error code. While in this example it might be feasible to write the code for TimeIt to handle unexpected input gracefully, e.g. by reporting an appropriate message, in other cases a check on preconditions may be critical. For example, COPYI is a piece of code taken from vyBase, the "portability glue" part of Voyager. The intention of the code is to provide a very quick copy routine for non-overlapping parts of integer vectors. A safe alternative would be to copy by element.

    VAR dest:ARRAY OF INTEGER;destoffs:LONGINT);
  BEGIN  FOR from:=srcoffs TO srcoffs+len DO

COPYISAFE would ignore negative length, and run into an index error if src or dest is too short. To gain speed, SYSTEM.MOVE can be used. But SYSTEM.MOVE is inherently unsafe. So it must be guarded by adequate checks.

  BEGIN  ASSERT(LEN(src)>=srcoffs+len-1,100);
    ASSERT((len>=0)&(len<(MAX(LONGINT) DIV sz)),102);

In this example, it is almost compulsory to use ASSERT. It would be hazardous to use SYSTEM.MOVE without testing for a legal input state.

Postconditions check the outcome at the end of a procedure. This may be a strict check, or it may be a reduced condition. For example, a procedure calculating the norm of a vector may end by checking the postcondition

just before exit. In many cases, reduced checks like this one may be sufficient. But in critical cases, the postcondition has to specify a strict condition for successful termination of an algorithm.

Strict postconditions tend to be rather complex and may require state information about the input or specific check routines. As an example, consider a sort algorithm operating on a chain of items
  ItemPtr=POINTER TO Item
    next: ItemPtr;
using an interface
  PROCEDURE sort(VAR first:ItemPtr);
A postcondition should at least verify that the result is actually sorted, and guard against the most common mistakes in sorting algorithms. For example, it should guard against dropping elements, or at least check that the number of elements is preserved. The latter may overlook duplication of elements at the cost of loss of others, so it is no strict check. But it is a necessary condition to be satisfied upon completion. To implement this check, a memory of the initial count and a check procedure for monotony is needed.
An implementation may have the skeleton
  PROCEDURE sort(VAR first:ItemPtr);
  VAR initialcount:LONGINT;
  PROCEDURE GetCount(from:ItemPtr):LONGINT;
    ... (* walk the chain and count *)
  END GetCount;
  PROCEDURE Sorted(from:ItemPtr):BOOLEAN;
    ... (* walk the chain and check order *)
  END Sorted;
    ... (* do the sort *)
  END sort;
At this point, we have to relax our recommendation:
  Never disable ASSERT
  unless you know why.

Even if the algorithm were correct and the ASSERT conditions can be proven to be always satisfied, it is very difficult for a compiler to identify that the variable initialcount and the procedures GetCount and Sorted are not needed. Given present compiler technology, it is a friendly gesture to the compiler to disable ASSERT and allow removal of dead code once the ASSERT can be considered proven.

For practical purposes, it may be easier to have test variables and test procedures in a "scaffold", and keep checks of the postconditions separate from the target code. For example, you can have a procedure sorttest, possibly in a separate module, with scaffold
  PROCEDURE sorttest(VAR first:ItemPtr);
  VAR initialcount:LONGINT;
  PROCEDURE GetCount(from:ItemPtr):LONGINT;
    ... (* walk the chain and count *)
  END GetCount;
  PROCEDURE Sorted(from:ItemPtr):BOOLEAN;
    ... (* walk the chain and check order *)
  END Sorted;
  END sorttest;
where "sort" is reduced to the proper sorting code. But this is just a pragmatic separation.

Loop invariants and loop variants
The postconditions in the example above have two components: a check on the count of the chain, to check consistency, and a check on the sorting order, to check termination. Neither check has been strict, but it is sufficient for this discussion. We will stay with this informal level.
As consistency and termination conditions are necessary at the end of a procedure, their counterparts are necessary conditions during execution. However, they take different roles.
We return to the sorting example. The consistency condition to keep the number of elements is necessary at all steps of the sorting process. Typically, sorting is an iteration through the chain to be sorted, possibly implemented in recursion. At each step, the condition
needs to be satisfied. If we want to safeguard against loss of information, an appropriate ASSERT
has to be added in the iteration loop. Conditions which have to be satisfied in each "iteration", or rather corresponding check variables, are usually called loop invariants.

On the other side, the termination condition
need only be satisfied at the end of the sorting process. During the sorting process, not all elements are sorted, i.e. there is a count "nrswaps" of unordered pairs in sequence which is zero if the queue is sorted, and is initialcount-1 at worst.

Sorting usually is implemented as a number of swaps of pairs or segments, and by looking at the algorithm it is not always clear that the algorithm will ever stop, let alone stop successfully. If termination is to be checked, we need a criterion to guarantee eventual termination. We can borrow a concept from other areas of mathematics. The general idea is that of a fixed point theorem. We need only the poor man's version: if we have a finite state space, and a transformation operating on this space, leaving it invariant, and an index which is bounded from below and reduced by applying a transformation, then an iterated transformation eventually stops at a fixed state. In short: if you walk down a finite ladder, you eventually hit the ground.
The general recipe for verifying that a process terminates is: establish that there is an invariant state space; that is, if you have to add subsidiary information, it does not grow beyond all bounds. Find an index which is never increasing, and guaranteed to be eventually decreasing. Under those conditions, the algorithm is guaranteed to end. The index used here is called a loop variant.

Ignoring the problem that an algorithm might introduce "fake elements", for our sorting problem the loop invariant
guarantees that our state space is finite: it corresponds to at most initialcount! permutations of our initial data set. If we have an algorithm which reduces the number of swaps, we have
for some ancillary variable nrswapsold, and if 0<= nrswaps we know that we can guarantee to stop eventually. Sometimes nrswaps may be not the best index. We may take into account of intermediate decrease of sorting order for some efficiency trade-off. But to get the general picture, this example may suffice.

Specify a condition which checks for stray duplication in a sorting process. If you cannot specify a strict condition, give a relaxed version.

Type invariants
Using object oriented programming, control flow may be more intricate than in classical procedural programming. While loop invariants/variants catch conditions in a step by step scenario, a corresponding strategy is needed for type specific invariants. A recommended way is to declare type specific procedures which check a type's invariant conditions, and use this in an ASSERT at the end of every procedure which must assert this invariant.

An example using ordinary procedures is to define
  PROCEDURE Invariant*(t:Type):BOOLEAN;
    RETURN condition
  END Invariant;
and use it as e.g.
  PROCEDURE Recalc*(obj: MyObject);
  END Recalc;
Using Oberon-2 type-bound procedures, the model is
  PROCEDURE (t:Type) Invariant()*:BOOLEAN;
    RETURN condition
  END Invariant;
and uses it as e.g.
  PROCEDURE (obj: MyObject) Recalc*;
  END Recalc;

Variable modes
A related problem should be mentioned here, although no general implementation model can be given. A common pre/postcondition of procedures refers to the role of variables. Oberon supports passing parameters by value and or by reference. Usually, the intended semantics is more specific.
  - parameters passed by value may be intended as input-only
    parameter, although Oberon would allow to use
    parameters passed by value as local (temporary)
    variables. For input-only parameters, the value
    may not be changed during procedure execution.
  - parameters passed by reference may be intended as
    output-only parameter. For output-only
    parameters, the execution of the procedure
    should not depend on the parameter values upon
    procedure entry; no initialization should be
(For efficiency reason, it is common to pass more complex structures by reference, where actually passing by value is intended. So the remark about input-only parameters applies to parameters passed by reference as well.)

There is no easy model to check this sort of conditions so far. At present, a recommendation is to add comments expressing the intended role, as in
  PROCEDURE abc ( (*in*) xyz: TypeIn);
  PROCEDURE cde (VAR (*out*) zyx: TypeOut);

Assertions: the big picture
On a low level, assertions can be considered a special debugging feature. With our interpretation, assertions aim at a more demanding target: to provide information to judge the correctness of a code. As such, they represent parts of the specification of a program. This representation is on code level and allows verification of these parts.
Ideally, a program can be seen as a series of transformations, transforming an input state satisfying certain conditions to a well-defined output state. If the postconditions define the output state, i.e. if we have strict postconditions, and if the postconditions can be derived formally for any input satisfying the preconditions, then we can prove that the program is correct. Loop invariants are landmarks to assert that we have not left the path, and loop variants provide milestones to see if we make any progress (or run in circles, or worse).
At present, we are far from reaching this goal of having proven correct programs. Nevertheless, this is a big picture to keep in mind as a goal.

In a program, we see both an intent and its implementation. The implementation is restricted by the formal rules of the programming language and the skill of the programmer. A traditional sideway is to add the intent as comments, escaping to a meta level. As the saying goes, comments are either wrong, or outdated, or both. Assertions offer a different possibly to express the programming intent in a way that guarantees consistency.
Considered this way, assertions are a possibility to imbed information about programming intent in the code in a way that can be recovered for documentation. Recovering the role from the code is too complicated for now. Instead, we have to rely on conventions. Unfortunately, these conventions are not universal. For example, Oberon System 3 and Oberon/F (aka Black Box) use conventions bases on the termination code:

  Oberon S3          Oberon/F
      free        0..19
  100..109  preconditions      20..59
  110..119  invariants      100..120
  120..129  postconditions      60..99
      reserved      121..125
      not yet implemented    126
      interface procedure called  127

Project exercise:
Write a "pretty printer" which is fail-safe. The pretty printer should work correctly on a correct Oberon source input, reasonable for "cut&paste" mess as an input, and allow extensions to cope with input from other languages.

You can take Mess.Mod from statlab.uni-heidelberg.de as a starting point. The general process is to parse the input text into low-level tokens, combine these to higher level tokens, and to rewrite them.
The strategy for fail-safe rewriting is to allow scratch parts. Any token may have a pre- or post-part which may be tokens, comments, or scratch.
The first role of assertions is to guarantee that no material is lost. So the combination part needs to be guarded by assertions.
The second role of assertions is to stabilize extensions. Mess.Mod allows the addition of "plug-ins". These plug-ins may install call-back functions.
As a master module, Mess has to safeguard against protocol violations of plug-ins which must work with source code other than Oberon source. So far, plug-ins are available for C and Pascal.

Allow one month for each of these tasks.
Allow half a year if working from scratch.

Part of this chapter has been adapted from S. H.-M. Ludwig's "Conventions for Programming". Thanks to G. Valiente and A. Fischer for hints and comments.

Einführung in die Programmiersprache Oberon. Kurs/Kap12.Text
gs (c) G. Sawitzki, StatLab Heidelberg

Introduction to the Oberon language. ItO/Ch12.Text
gs (c) G. Sawitzki, StatLab Heidelberg

Home Up Intro Contents Chapter 1 2 3 4 5 6 7 8 9 10 Design Assert Timing EBNF Report Pas