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

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:

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

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