invariant

Summary#

An invariant is a rule about the whole row, enforced when the row is written. A constraint speaks about one member ([Max(5)] int Priority); an invariant speaks about the relationship between members — and can be conditional, so it applies only to the rows it should.

Signature#

entity <Name> {
  invariant <condition>;                                       // always holds
  invariant <condition> when <guard>;                          // holds only for rows where <guard> is true
  invariant <condition> when <guard> message "<explanation>";  // …and say why, when it fails
}

Description#

How do I write a rule over the whole row?#

The condition is written over the row's own members, and must be true when the row is written:

entity Account {
  [Required] string Holder;
  decimal Balance;
  invariant Balance >= 0;
}

Any code path that would leave Balance negative — a withdrawal, an import, an adjustment — fails at commit. You do not have to remember to check it, and neither does the next person.

A rule that applies to some rows#

when guards the invariant. The rule is only checked for rows where the guard is true, so one entity can hold several kinds of row without the rules of one contaminating the others:

entity Product {
  [Required] string Name;
  bool IsPerishable;
  int ShelfDays;

  invariant ShelfDays <= 30 when IsPerishable
    message "Perishable items can have at most 30 shelf days.";
}

A tin of beans with ShelfDays = 400 is fine — the guard is false, so the rule never fires. Milk with the same value is rejected, and the person who tried gets the sentence you wrote rather than a constraint name.

How do I say why it failed? — message#

message is the explanation a human sees. Without it they get a rule that says ShelfDays <= 30, which tells them what was violated but not what to do. Write the message as though you are talking to the person who hit it — because you are.

What an invariant can see#

The row it is on, and one row it references. An invariant reads the members of its own entity, and may read through a [Required] reference to the row it names — one step, no further. It does not run a query, it does not read a collection, and it does not call a function — writing one there is refused with the reason. That is what keeps it cheap enough to check on every write. It may use your consts (a constant is a literal by another name, so the rule and a function that explains it can share one pattern) and the built-in text and Regex operations — a query over a sequence the rule builds itself included, such as Options.Split("\n").Any(o => o.Trim() == Choice).

How do I write a rule that depends on another row?#

Read through the reference. An answer's shape depends on its field's kind, which lives on the field's row:

enum AnswerKind { Text, Number }

entity Question {
  [Required, MaxLength(100)] string Name;
  AnswerKind Kind;
}

entity Answer {
  [Required] Question Question;
  [Required, MaxLength(200)] string Value;
  invariant Regex.IsMatch(Value, "^[0-9]+$") when Question.Kind == AnswerKind.Number
    message "This question takes a number.";
}

The rule is checked against the referenced row as the commit will leave it: if the same unit of work changes the question's kind and writes an answer, the answer is judged by the new kind.

Three things are refused, each with the fix in the message:

• Two steps — Warehouse.Region.Open reads a row the written row does not name. Put the part about the region on Warehouse, where that row is written, or check it in the function that writes the row.
• A reference that may be empty, with nothing said about it — on a row without one the rule would read null and refuse the write. Make the reference [Required], or say what holds without one: invariant Spillover == null || Spillover.AcceptsHazardous;, … when Spillover != null, or Spillover?.….
• A collection — many rows. Check it in the function that writes the row.

Reading a referenced row's Id is not a step: ToVersion.Application.Id == Application.Id reads the written row and the version, which holds the application's id itself.

What happens when the referenced row changes?#

The rule guards the row being written. Changing the question's kind later does not re-check the answers that already point at it — they were valid when they were written, and they are not written again. If a change to the referenced row must not leave its referencing rows behind, refuse that change where it is made: make the member [Immutable], or check it in the function that changes it.

Who it holds for — every write#

An invariant holds whoever writes the row: a visitor's function, staff on a desk, and a workflow too — a workflow runs your code as the system, and the system skips the rest of validation the way it skips security, but never a rule you declared as always true. A workflow step that would leave Stock below zero is refused like any other write, and the row stays as it was. It cannot call a function of yours (see What an invariant can see above) — a check that needs one belongs in the function that writes the row.

It is also judged on every update, whichever members the update changes. That is the difference from a single-member constraint, which an update judges only when it changes that member ([[entity-constraints#on-update]]): an invariant spans members, so changing one of them can break it. invariant Start <= End; refuses an update that moves only Start past End. A rule with a when guard is judged on every write for the same reason — the guard reads other members.

See also#

• constraints — the single-member rules ([Required], [Unique], [Min]/[Max], [Pattern])
• entity members — the members an invariant reads
• entity — the entity an invariant guards