Predefined Pre- and Postcondition Qualifiers

The following qualifiers are predefined in the Fuzion standard library. They are used within the standard library itself, but they are also available for use in library modules or Fuzion application code.

• safety

  This qualifier protects preconditions that are required for the safety of an operation.

  An example is the index check precondition of the intrinsic operation to access an element of an array: Not performing the index check would allow arbitrary memory accesses and typically would break the applications safety.

  This qualifier should therefore never be disabled unless you are running code in an environment where performance is essential and safety is irrelevant.

• debug

  This qualifier is generally meant for debugging, it is set when debugging is enabled.

• debug(n)

  This qualifier enables checks at a given debug level. A higher level enables additional, typically more expensive checks compared to a lower level.

• pedantic

  This qualifier is for conditions that a pedantic purist would require. A more relaxed hacker would prefer to do without this qualifier.

• analysis

  This is a qualifier for conditions that are generally not reasonable as runtime checks. Either because they are prohibitively expensive or even not at all computable in this finite universe. These conditions may, however, be very useful for formal analysis tools that do not execute the code but perform techniques such as abstract interpretation or formal deduction to reason about the code.