Fuzion Logo
fuzion-lang.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 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
  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.:

sqrt(a i32) i32
  debug ==> a >= 0,
  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

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)
  analysis ==> for_all<u32>(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