12. Contracts

Contracts fail fast. They describe assumptions or completion guarantees; ordinary validation libraries remain appropriate when an application needs several user-facing errors at once. Write require or ensure with its condition first. The compiler supplies the default exception and diagnostic message; do not repeat the condition in otherwise text. Use otherwise only for a useful different explanation or an intentional exception choice.

12.1 Immediate requirements

CS-CONTRACT-001. require checks at its execution point and throws immediately on failure. It does not accumulate validation errors.

CS-CONTRACT-002. A Boolean condition must be true. A bare reference requires presence; a bare String or collection requires a usable nonempty value. A bare number is not a positive/nonzero guard: write the numeric condition.

action Register(customer as Customer, limit as Decimal)
    require customer
    require customer.Email is not whitespace
    require limit >= 0

    customer.ApproveLimit(limit)
end action

The Customer contract assumes an Email property and the ApproveLimit action from chapter 9. Reaching the first failing requirement prevents subsequent statements from running.

12.2 Failure customization and exception category

CS-CONTRACT-003. Default failures use standard .NET exception categories:

Failure	Default exception
Required action parameter is nothing	ArgumentNullException with its actual parameter name
Clearly attributable parameter constraint	ArgumentException, or an appropriate standard subclass when justified
State requirement or complex condition without clear parameter attribution	InvalidOperationException
Failed ensure, including one mentioning a parameter	InvalidOperationException

CS-CONTRACT-004. otherwise supplies a custom message or exception expression. A message retains the contextual exception category. An explicit exception expression supplies its chosen exception. Compiler-produced messages include the failed source expression as a stable searchable suffix, omit potentially confidential runtime values, and must not evaluate a condition again merely for formatting.

require customer.IsActive otherwise "Only active customers can place orders"
require customer.IsActive otherwise new Global.System.InvalidOperationException()
ensure result is not nothing otherwise "An approved order must include a receipt"

Failure expressions run only on failure. otherwise is not an arbitrary statement block or another else construct. Presence expression ?? throw belongs to expression semantics and is independent of contract customization.

12.3 Normal-exit postconditions

CS-CONTRACT-005. ensure declares a condition checked on normal action completion, including early return, bare return and fallthrough. Reaching its declaration does not check it immediately.

CS-CONTRACT-006. result denotes the captured value being returned. A postcondition must not cause reevaluation of the original return expression.

CS-CONTRACT-007. Propagating exceptions skip action postconditions. Required nested/enclosing finally blocks complete before action-level postconditions check final state. If cleanup throws, normal completion is abandoned and the postconditions do not run.

CS-CONTRACT-008. Postcondition failure throws and prevents successful return. Postconditions must not be lowered into an unconditional C# finally, which would incorrectly execute them during propagation.

public class Account
    Balance as Decimal with private set = 0

    constructor(balance as Decimal)
        require arguments.balance >= 0
        Balance = arguments.balance
    end constructor

    action Withdraw(amount as Decimal)
        returns Decimal

        require amount > 0
        require Balance >= amount
        ensure Balance >= 0
        ensure result = Balance

        Balance -= amount
        return Balance
    end action
end class

The returned Decimal is captured after the mutation. A cleanup block that changes Balance before completion is visible to the postcondition. A cleanup failure propagates through ordinary exception rules instead of being reclassified as a contract failure.

12.4 Entry snapshots

CS-CONTRACT-009. old_value_of(source) denotes a value captured at action/constructor entry. Repeated references to an eligible source denote the same entry value, not later evaluation. Snapshots may be used in ordinary logic, logging and auditing as well as postconditions. They snapshot the value, not an independent deep object graph.

Action entry capture occurs before all authored body statements, including require guards. A referenced snapshot getter can therefore execute even if a subsequent guard fails. A failure during capture propagates before the body and guards run; it is not converted into a contract failure. Later uses read the captured value without reevaluating the source. Capture is not delayed until validation succeeds or until the first runtime use of old_value_of.

Capture distinct eligible sources in order of their first written old_value_of occurrence in the current action or constructor, once per source. Repeated occurrences reuse that capture. If a capture fails, do not evaluate later captures or execute the body. The reads are sequential, not an atomic snapshot of the object graph. A separately declared local action establishes its own capture list and entry time.

Constructor entry means the point after generated initialization and immediately before that constructor's authored body. Preserve the construction sequence: member declaration initialization, delegation/base construction, need validation/storage, promoted-property assignment, snapshot capture, authored body and its require guards. Thus a promoted property supplied as 100 is captured as 100 before the body changes it. A member whose required initialization occurs only later in the body, such as an otherwise uninitialized readonly member, is unavailable for an entry snapshot. Its raw CLR storage default must not be substituted for initialized state. Mutable members already initialized to their normal DirectSharp defaults remain eligible.

For same-class delegation, capture the delegating constructor's own sources after the delegated constructor returns and before its own body starts. Do not rerun member initializers. Each constructor has its own capture list. Capture failure prevents its body/guards from running but does not undo earlier initialization or delegation; construction is not a transaction.

CS-CONTRACT-010. The operand must be a simple value source available at entry to the current action or constructor: effective parameter, accessible field/property/member chain, or an already-available captured outer local. A local declared inside the current action/constructor is ineligible, even if old_value_of appears after that declaration. The compiler must reject it rather than snapshot at declaration time or fabricate a pre-declaration value. Arbitrary arithmetic, action/method invocation, constructor calls and side-effecting indexer computations are rejected.

ensure account.Balance = old_value_of(account.Balance) - amount

This action-level fragment assumes an Account parameter and an amount parameter. It compares final balance with entry balance. old_value_of(amount + tax) and old_value_of(GetBalance()) are invalid executable expressions rather than simple sources.

action Example(amount as Integer)
    let initial = amount
    Global.System.Console.WriteLine(old_value_of(initial)) // invalid: initial did not exist at entry
end action

Use old_value_of(amount) for the parameter's entry value. If an application needs a later snapshot, assign that value to an ordinary named local at the desired point; old_value_of does not acquire a different meaning for body locals. A captured outer local is captured when the current local action is entered, not when that local action is declared.

For a present Account with Decimal Balance and Limit properties, this audit fragment captures Balance first, then Limit:

action AuditEntry(account as Account)
    Log(old_value_of(account.Balance))
    Log(old_value_of(account.Limit))
    Log(old_value_of(account.Balance))
end action

Reference C# lowering, with the same application Log action:

public void AuditEntry(Account account)
{
    decimal __oldBalance = account.Balance;
    decimal __oldLimit = account.Limit;
    Log(__oldBalance);
    Log(__oldLimit);
    Log(__oldBalance);
}

The captures precede all three Log calls. The repeated Balance reference does not rerun its getter. If the first capture throws, neither the Limit getter nor any Log call executes.

12.5 Reference lowering and diagnostics

For Withdraw without intervening cleanup:

public decimal Withdraw(decimal amount)
{
    if (amount <= 0m)
        throw new ArgumentException("Requirement failed: amount > 0", nameof(amount));
    if (Balance < amount)
        throw new InvalidOperationException("Requirement failed: Balance >= amount");

    Balance -= amount;
    decimal result = Balance;
    if (Balance < 0m)
        throw new InvalidOperationException("Postcondition failed: Balance >= 0");
    if (result != Balance)
        throw new InvalidOperationException("Postcondition failed: result = Balance");
    return result;
}

Multiple returns require normal-completion routing after applicable cleanup. An exceptional path bypasses the postcondition epilogue. Diagnostic obligations include an invalid condition type; incompatible failure expression; invalid result use in a resultless context; forbidden snapshot expression; and access to a source unavailable at entry. Exact compiler diagnostic codes and punctuation are independent of these obligations.

Specification contents · Previous: 11. Enums, flags and one-of types · Next: 13. Exceptions