Invariant

An invariant is a logical expression that must always hold true. Invariants validate state changes in entities, or parameter values in functions.

Syntax

As of RIDDL 2.0 an invariant's condition may be a structured boolean expression, not only an opaque quoted string:

invariant BalanceNonNegative is balance >= Zero
invariant InStock             is quantity > Zero
invariant Legacy              is "the account must be in good standing"

The quoted form remains available for rules that genuinely resist structure.

Because comparisons are reference-only, a threshold is named rather than written inline:

constant Zero is Natural = "0"
invariant BalanceNonNegative is balance >= Zero

State-Scoped Invariants

An invariant may be declared inside an entity state body, where it constrains that state's record-shaped data:

entity Account is {
  initial state Open of record OpenData is {
    invariant BalanceNonNegative is balance >= Zero

    handler H is { ??? }
  }

  state Closed of record ClosedData is {
    invariant BalanceIsZero is balance == Zero
  }
}

This is what lets different states carry different rules — an open account may hold any non-negative balance, while a closed one must hold exactly nothing. An invariant declared at entity level instead applies in every state.

Referencing an Invariant

A handler asserts an invariant by name:

on command Withdraw {
  require invariant BalanceNonNegative
  ???
}

Validation

An invariant defined but never referenced by any require invariant statement draws a UsageWarning. Declaring a rule the model never checks is almost always an oversight.

Occurs In

• Any processor — entities, contexts, repositories, projectors, adaptors, streamlets
• An entity state body
• Modules

Contains

Nothing — but its condition is a value.