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 set when compiling a Fuzion application, so we can choose between a debug- and a production version with different levels of runtime checks.

Alternatively, one can use a dedicated debug flag example_debug that could then be enabled or disabled manually to have local debug checks:

Setting it to false will disable these checks:

or setting it the global debug level will use the global default:

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: