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.
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 envirnment where performance is essential and safety is irrelevant.
This qualifier is generally for debugging, it is set iff debugging is enabled.
this qualifier is specific for enabling checks at a given debug level, where higher levels include more and more expensive checks.
This qualifier is for conditions that a pedantic purist would require, that otherwise a more relaxed hacker would prefer to do without.
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.
⮫ next: Invariants