Source status: no status is stated in the source document, so none is assigned here. Do not treat this page as a finalized specification. The normative rules are in the Technical Specification.

First Language Example: Bank Account¶

Objective¶

Create a bank account module that supports deposits and withdrawals while enforcing financial rules.

Source Code¶

MODULE BankAccount

TYPE Account:
    balance: Decimal
    INVARIANT balance >= 0

FUNCTION deposit(
    account: Account,
    amount: Decimal
) -> Result<Account, DepositError>

    REQUIRES:
        amount > 0

    ENSURES:
        result.balance == OLD(account.balance) + amount

    EFFECTS:
        MODIFY account.balance

    FAILURES:
        InvalidAmount

    IMPLEMENTATION:
        account.balance = account.balance + amount
        RETURN SUCCESS(account)


FUNCTION withdraw(
    account: Account,
    amount: Decimal
) -> Result<Account, WithdrawalError>

    REQUIRES:
        amount > 0
        amount <= account.balance

    ENSURES:
        result.balance == OLD(account.balance) - amount

    EFFECTS:
        MODIFY account.balance

    FAILURES:
        InvalidAmount
        InsufficientFunds

    IMPLEMENTATION:
        account.balance = account.balance - amount
        RETURN SUCCESS(account)

END MODULE

Required Compiler Checks¶

The compiler should check:

1. An account balance cannot become negative.
2. Deposits must increase the balance by exactly the deposited amount.
3. Withdrawals must decrease the balance by exactly the withdrawn amount.
4. Negative and zero transaction amounts must be rejected.
5. Withdrawals cannot exceed available funds.
6. All declared failure conditions must be handled.
7. Functions cannot modify undeclared state.
8. Successful operations must satisfy their postconditions.

Verification Tests¶

Success Criteria¶

The prototype must demonstrate that invalid implementations are rejected, valid implementations can be compiled, and verification results accurately distinguish proven properties from unverified ones.

A program passing these checks must not automatically be considered completely correct. Only the specified properties have been evaluated.

Source and authority¶

This page migrates FIRST_MODULE.md in full. It is an explanatory / implementation document, not the normative specification. Where it simplifies a rule, the Technical Specification governs. The original file is preserved in source-original/LANG/.