Skip to content

About this page: this page is editorial guidance written for this documentation site. It summarises and links to source material; it defines no language rules. The normative rules are in the Technical Specification.

Examples

The source material contains one worked example:

  • First program: Bank Account — a bank account module with deposits and withdrawals, invariants (balance >= 0), contracts, and a verification test table. This is the MVP's first demonstration program.

Examples are not normative

Examples illustrate intended behaviour; they do not define language rules. Where an example uses a syntax or behaviour that the specification leaves open, the open decision governs — see Section 57.