Invariants

Classes and Records can define optionally define invariants – boolean conditions that will automatically be enforced to be true by the compiler.

Invariants together with Pre- and Post-Conditions in Methods are part of part of Oxygene's Class Contracts feature that enables Design by Contract-like syntax to create self-testing types.

Invariants are used to define a fixed state an instance of the type must fulfill at any given time.

Invariants are declared in a special section of the class or record type initiated with the invariants keyword. Inside the invariants section, zero or more boolean expressions can be listed, separated by semicolon. At certain times during the execution of the program (more on that below), these expressions will be evaluated, and execution will abort with a fatal Assertion, if one of them fails (i.e., evaluates to false).

type
  MyClass = class;
  public
    ... some methods or properties
  public invariants
    fField1 > 35;
    SomeProperty = 0;
    SomeBoolMethod() and not (fField2 = 5);
  private invariants
    fField > 0;
  end;

Invariants can provide an optional more detailed error message, to be included in the assertion when a check fails. This must be in the form of a constant String Literal, separated from the expression with a colon. If the expression itself contains a colon, the whole expression needs to be wrapped in parenthesis:

public invariants
  (SomeValue:SomeField = 0) : "SomeField may not be zero!";

Public vs. Private Invariants

Invariants can be marked either public or private.

Public invariants will be checked at the end of every non-private method call or property access, and if an invariant fails, an assertion is raised.

Private invariants will be checked at the end of every method call, including private methods.

The idea behind this separation is that that public invariants must be met whenever a call is made into the type from the outside. In other words, no outside access to the type should ever leave the object in an invalid state.

However, there might be certain scenarios where a public method defers work to two or more private methods; the first of those calls might leave the object in a partial state, which the second call then rectifies. If all invariants were checked at every step, this would be a problem.

You can think of private invariants as being most strict. Any time a method finishes, they must be satisfied to the T. Public invariants are more lax – anything goes while the type does its work internally, eve across multiple methods. But when it is done and execution passes back to an outside caller, these invariants too must be sorted out again.

Note that both types of invariant sections have full access to all private fields of the class, the only difference is the method (and property) calls they apply to.

If a class specifies invariants, all fields must be marked as private.

About Assertions

Note that like pre- and post-conditions, invariants will only be compiled and executed if the "Enable Asserts" Compiler Option is on. By default, this option is off for Release builds, to optimize performance. It is important to not rely on invariants to execute for the regular operation of the project, and to avoid conditions with side effects.

Pre- and post-conditions should be used only for testing, not for general code flow.

See Also