Fuzion Logo
fuzion-lang.dev — The Fuzion Language Portal

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
pre
  debug : a >= 0,
post
  debug : result >= 0,
  debug : result * result <= a,
  debug : a - result * result <= 2*result
=>
  ...

This flag could be enabled globally by a compiler switch (-debug 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

Analysis

sort(a array i32)
inv
  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

last changed: 2025-01-29