Fuzion Contracts

Fuzion supports design by contract as was introduced originally in the [[https://www.eiffel.com/|Eiffel]] programming language.

As an example, let's define a function to calculate the square root of a 32-bit integer value:

  i32 sqrt(i32 a)
    req a >= 0;
    ens result >= 0;
        result * result <= a;
        a - result * result <= 2*result;
  {
    result = 1;
    while (result > a / result) || (a - result * result <= 2*result)
    {
      result = (result + a / result) / 2;
    }
  }

Open questions:

• 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.:

  i32 sqrt(i32 a)
    req
      debug ==> a >= 0;
    ens
      debug ==> result >= 0;
      debug ==> result * result <= a;
      debug ==> a - result * result <= 2*result;
  {
    ...
  }

This flag could be enabled globally by a compiler switch ("-Ddebug=true" or similar), or locally by adding a flag locally

  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

Analysis

  sort(array a)
    ens
      analysis ==> forAll(fun (u32 x) -> x < a.length-1 ==> a[i] <= a[i+1]);
  {
  ...
  }

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