Fuzion Logo
flang.dev — The Fuzion Language Portal
JavaScript seems to be disabled. Functionality is limited.

Developing with pre- and postconditions

The pre- and postconditions are a part of a feature's signature, not of its implementation. Ideally, we should start describing every feature's signature, including pre- and postconditions, before we implement it. In the case of the sqrt function above, this should have been

Ideally, the legal inputs and the results and effects of features can be fully described by their signature. In practice, however, a natural language description is also helpful or even required. Also, many conditions would be very expensive to verify. See the following example of a feature that modifies a value in an array:

The postcondition in this example is particularly expensive for large arrays. We probably do not want to check it at runtime unless we are debugging this part of the code. So we need some fine grain control over which conditions to check.

One way to use fine grain control is to add a qualifier in front of the condition, e.g., using the debug qualifier:

This qualifier is defined globally and can be when compiling a Fuzion application, so we can chose between a debug- and a production version with different levels of runtime checks.

Alternatively, these checks could manually be enabled or disabled for certain features by defining a debug field locally and setting it to true

or setting it to false to disable these checks:

We can also distinguish different debug levels and, e.g., enable preconditions in the first debug level, add cheap postconditions in the second, but disable expensive ones for all levels less than 10: