Fuzion supports design by contract as was introduced originally in the Eiffel programming language.
As an example, let's define a function to calculate the square root of a 32-bit integer value:
sqrt(a i32) i32 pre a >= 0 post result >= 0, result * result <= a, a - result * result <= 2*result is result := 1 while (result > a / result) || (a - result * result <= 2*result) result := (result + a / result) / 2
- When can pre- and postcondition checking be disabled? For production code, or only for unsafe high-performance code?
- Some conditions can be very expensive, e.g., iterating over an array to check some property. Do we need different levels for conditions of different complexity?
- Some conditions may not be executable at all, e.g., requiring ∃ or ∀ quantors and being useful only for abstract interpretation as, e.g., in the Java Modeling Language. How should these be marked?
Disabling / Enabling Checks
Global flags could enable / disable checks, e.g.:
sqrt(a i32) i32 pre debug ==> a >= 0, post debug ==> result >= 0, debug ==> result * result <= a, debug ==> a - result * result <= 2*result is ...
This flag could be enabled globally by a compiler switch ("-Ddebug=true" or similar), or locally by adding a flag
sqrt.debug := true;
Several categories can provide different levels of checks
- safety -- for checks that are required to avoid crashes, such as array out of bounds
- debug -- for debugging, maybe with different, user defined debug levels
- analysis -- never checked at runtime, for formal analysis only
sort(a array i32) inv analysis ==> forAll<u32>(fun (u32 x) -> x < a.length-1 ==> a[i] <= a[i+1]) is ...
Relation to System Requirements
Here is an article about formal system requirements. It should be possible to map formal system requirements to Fuzion contracts: The role of formalism in system requirements