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
: