Assertion (computer science)

from Wikipedia, the free encyclopedia

An assurance , assurance or assertion ( Latin / English for statement , assertion ) is a statement about the state of a computer program or an electronic circuit . With the help of assurances, logical errors in the program or defects in the surrounding hardware or software can be recognized and the program terminated in a controlled manner. When developing electronic circuits, assertions can be used to check compliance with the specification in the verification phase. Furthermore, assertions can provide information about the degree of test coverage during the verification.

application

By formulating an assurance, the developer of a program expresses his or her belief in certain conditions during the life of a program and makes them part of the program . He separates these beliefs from the normal running time circumstances and accepts these conditions as always true. Deviations from this are not dealt with regularly so that the large number of possible cases does not prevent the solution of the problem, because of course it can happen during the runtime of a program that 2 + 2 = 4 does not apply B. because variables were overwritten by a program error in the operating system.

Thus assurances differ from the classic error control through control structures or exceptions ( exceptions ) that a fault as a possible outcome include . In some programming languages , assurances have been built into the language level; they are often implemented as a special form of exception .

Error handlers should be written for error conditions that are expected; Assurances for error conditions that should never occur.

history

The term assertion was introduced by Robert Floyd in 1967 in his article Assigning Meanings to Programs . He proposed a method for proving the correctness of flowcharts by giving an assurance to each element of the flowchart. Floyd provided rules by which representations could be determined. Tony Hoare further developed this method for the Hoare calculus for procedural programming languages . In Hoare logic an assurance that precedes an instruction is prerequisite (English precondition ), a representation according to an instruction postcondition (English postcondition called). An assurance that must be fulfilled every time the loop is run is called an invariant .

Niklaus Wirth used assurances to define Pascal's semantics and suggested that programmers write comments with assurances in their programs. For this reason, comments in Pascal are surrounded by curly braces {…}, a syntax that Hoare used for assertions in his calculus.

The idea was adopted in Borland Delphi and is incorporated as a system function assert. In the Java programming language , the keyword assertis available from version 1.4 .

The hardware description languages ​​VHDL and SystemVerilog used to develop electronic circuits support assertions. PSL is a stand-alone description language for assertions that supports models in VHDL, Verilog and SystemC . During the verification, the simulation tool records how often the assertion was triggered and how often the assurance was fulfilled or violated. If the assertion was triggered and the assurance was never violated, the circuit is considered to have been verified successfully. However, if the assertion was never triggered during the simulation, there is insufficient test coverage and the verification environment must be expanded.

Programming practice

In the C programming language , an assurance could be used something like this: 

#include <assert.h>
/// diese Funktion liefert die Länge eines nullterminierten Strings
/// falls der übergebene auf die Adresse NULL verweist, wird das
/// Programm kontrolliert abgebrochen. (strlen prüft das nicht selbst)
int strlenChecked(char* s) {
  assert(s != NULL);
  return strlen(s);
}

In this example, the macro can be used by including the header file assert.h . In the event of a failure, this macro issues a standard message in which the condition that has not been met is quoted and the file name and line number are added. Such a message could look like this: assert

Assertion "s!=NULL" failed in file "C:\Projects\Sudoku\utils.c", line 9

Java knows the concept of assurances from version 1.4. Here, however, the program is not necessarily complete, but a so-called exception (English exception triggered), which can be further processed within the program.

A simple example of an assertion (here in Java syntax ) is 

int n = readInput();
n = n * n; //Quadrieren
assert n >= 0;

With this assertion the programmer says "I am sure that after this point n is greater than or equal to zero".

Bertrand Meyer processed the idea of ​​assurances in the programming paradigm Design by Contract and implemented it in the programming language Eiffel . Preconditions are described by require clauses, postconditions by ensure clauses. Invariants can be specified for classes. Exceptions are also raised in Eiffel if an assurance is not met.

Related techniques

Assertions detect program errors at runtime at the user, i.e. only when it is too late. In order to avoid messages about "internal errors" as far as possible, attempts are made to have logical errors detected in the form of errors and warnings at compile time (by the compiler ) by means of suitable formulation of the source text . Logical errors that cannot be found this way can often be uncovered using module tests .

Reformulating the source code

By reducing case distinctions to a minimum, some errors cannot be expressed. Then it is also not possible as a logical error. 

// Kurvenrichtung
public enum TURN { LEFT_TURN, RIGHT_TURN }

// Methode liefert den Text zu einer Kurvenrichtung
public String getTurnText(TURN turn) {
  switch(turn) {
    case LEFT_TURN: return "Linkskurve";
    case RIGHT_TURN: return "Rechtskurve";
    default: assert false: "Es gibt nur Links- oder Rechtskurven"; // Kann nicht auftreten
  }
}

Assuming that there were only the two cases (in fact often they are), then we could use a simple truth value instead of a more specialized coding: 

// Methode liefert den Text zu einer Kurvenrichtung
public String getTurnText(boolean isLeftTurn) {
  if (isLeftTurn) return "Linkskurve";
  return "Rechtskurve";
}

In many cases, as in this example, this makes the code less explicit and therefore more incomprehensible.

Compile-time assurances

While the assertions described above are checked when the program is running, in C ++ there is the option of checking conditions when the program is compiled by the compiler . Only conditions that are known at compile time can be checked, e.g. B. sizeof(int) == 4. If a test fails, the program cannot be compiled: 

#if sizeof(int) != 4
  #error "unerwartete int-Größe"
#endif

In the past this depended heavily on the functionality of the respective compiler and some formulations took some getting used to: 

/// Die Korrektheit unserer Implementierung hängt davon ab,
/// dass ein int 4 Bytes groß ist. Falls dies nicht gilt,
/// bricht der Compiler mit der Meldung ab, dass
/// Arrays mindestens ein Element haben müssen:
void validIntSize(void) {
  int valid[sizeof(int)==4];
}

With C11 and C ++ 11, the keywords _Static_assert and static_assert (additionally implemented as a macro in C11) were introduced to solve this problem : 

//in C als auch C++
void validIntSize(void) {
  static_assert(sizeof(int)==4,
    "implementation of validIntSize does not work with the int size of your compiler");
}

Assurances in module tests

One area in which assurances also play a role are module tests (including a core component of extreme programming ). Whenever you make changes to the source code (e.g. refactorings ), e.g. B. in order to integrate further functions, tests are carried out on partial functions (modules, e.g. functions and procedures, classes) in order to evaluate the known (desired) functionality.

In contrast to assert, if the program fails, the entire program is not terminated, only the test is considered to have failed and further tests are carried out in order to find as many errors as possible. If all tests run without errors, it should be assumed that the desired functionality exists.

Of particular importance is the fact that module tests are usually not carried out in the productive code, but rather at development time. This means that assertions are to be seen as counterpart in the finished program.

Special techniques for Microsoft compilers

In addition to Assert, Verify is also used. Verify executes all statements that go into the calculation of the condition, regardless of whether it was compiled with or without intent to debug. The check only takes place in the debug version, i.e. H. Here, too, a program can fail in an obscure way if the promise is not fulfilled. 

// die Variable anzahl wird immer erhöht
Verify(++anzahl>2);

Assert_Valid is used to test objects for their validity. There is also the virtual method in the base class of the object hierarchy AssertValid(). The method should be overwritten for each specific class in order to test the validity of the internal fields of the class. 

// Example for CObject::AssertValid.
void CAge::AssertValid() const
{
  CObject::AssertValid();
  ASSERT( m_years > 0 );
  ASSERT( m_years < 105 );
}

literature

  • Robert W. Floyd: Assigning meanings to programs . In: Proceedings of Symposia in Applied Mathematics , Volume 19, 1967, pp. 19-32.

Web links

Individual evidence

  1. ↑ Steve McConnell: Code Complete. A Practical Handbook of Software Construction . Ed .: Microsoft Press. 2nd Edition. 2004, ISBN 978-0-7356-1967-8 (English).