Section 3: Functions and Contracts¶

TECHSPEC-03 — Section 3 · Version 0.1 · Status: Initial Draft

Status: draft. This section is an Initial Draft (Section 57 is a Working Register). It describes intended or proposed behavior, not a finalized, implemented language rule. Do not treat examples here as normative.

1. Function Declaration¶

Every function must explicitly declare: - Name. - Parameters and their types. - Return type. - Preconditions. - Postconditions. - Side effects. - Possible failure outcomes. - Implementation.

Example:

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

    REQUIRES:
        amount > 0
        amount <= account.balance

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

    EFFECTS:
        MODIFY account.balance

    FAILURES:
        InvalidAmount
        InsufficientFunds

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

END FUNCTION

2. Preconditions (REQUIRES)¶

Preconditions describe what must be true before a function executes.

Rules: - Preconditions must be explicitly declared. - Preconditions must be evaluated before implementation. - A function must not execute when its preconditions are violated. - Callers are responsible for establishing the required conditions. - Preconditions must not be treated as guarantees about the function's output.

3. Postconditions (ENSURES)¶

Postconditions describe what must be true after successful execution.

Rules: - Postconditions must be evaluated against the resulting program state. - They apply only to the outcomes they explicitly describe. - A successful function must satisfy every applicable postcondition. - Failed postconditions constitute contract violations. - The compiler must distinguish proven postconditions from runtime-checked postconditions.

4. Invariants¶

Invariants describe conditions that must remain true throughout the lifetime of an object or defined state.

Example:

TYPE Account:
    balance: Decimal

    INVARIANT:
        balance >= 0

Rules: - Invariants must hold whenever an object is in a valid observable state. - Operations modifying protected state must preserve applicable invariants. - Invalid state transitions must be rejected or prevented.

5. Previous State (OLD)¶

OLD(expression) refers to the value of an expression immediately before function execution.

Rules: - OLD may only be used in postconditions. - Its value must remain available during verification. - It must represent the original state, not a subsequently modified value.

6. Side Effects (EFFECTS)¶

Functions must declare every external or shared state modification.

Initial effect categories:

• READ: Read external or shared state.
• MODIFY: Change external or shared state.
• CREATE: Create external resources.
• DELETE: Remove external resources.
• NETWORK: Communicate with external systems.

Undeclared effects must be rejected.

7. Failure Outcomes¶

Functions must explicitly declare possible expected failures.

Rules: - Every declared failure must have a defined error type. - Failure outcomes must be represented in the return type. - Callers must handle or explicitly propagate failures. - A failed operation must not be reported as successful. - Unexpected contract violations must remain distinguishable from declared failures.

8. Verification Requirements¶

The compiler must evaluate function contracts using available verification methods.

It must distinguish: - PROVEN: The property has been formally established. - CHECKED: The property has been evaluated through an applicable check. - UNVERIFIED: The property could not be established. - FAILED: The property was violated.

A declaration alone is never evidence that its guarantee is satisfied.

9. Design Goal¶

Every function must communicate exactly what it expects, what it is allowed to change, what it promises, and how it can fail.

AI-generated implementations must be checked against these declarations rather than trusted to fulfill them.

Source and related sections¶

Source file: TECHSPEC-3.md (preserved in source-original/LANG/). See the specification index, the glossary, and the cross-reference index.