Class Contracts

From RemObjects Software

This is a Oxygene Language Feature topic
Feel free to add your notes to this topic below.

Oxygene introduces two new language constructs to enable design by contract like features:

• Pre-conditions and Post-conditions
• Invariants

If a contract is not upheld, an assertion is generated. See assert (Compiler Magic Function) for how assertions work and how to control when class contracts are enabled.

Pre-conditions and Post-conditions

Pre and post conditions are used to describe conditions that are required to be true when a method is called or after a method exits, respectively. They can be used to check for the validity of input parameters, results, or for the state of the object required by the method.

The require and ensure keywords will expand the method body to list the preconditions; both sections can contain a list of Boolean statements, separated by semicolons.

Examples:

method MyObject.DivideBy(aValue: Integer);
require
  aValue <> 0;
begin
  MyValue := MyValue/aValue;
end;

method MyObject.Add(aItem: ListItem);
require
  assigned(aItem);
begin
  InternalList.Add(aItem);
ensure
  Count = old Count +1;
End;

method MyObject.DoWork(aValue);
require
  Assigned(fMyWorker);
  fMyValue > 0;
  aValue > 0;
begin
  //... do the work here
ensure
  Assigned(fMyResult);
  fMyResult.Value >= 5;
end;

The 'old' scope prefix can be used in the 'ensure' section for local variables and parameters to refer to the original values before the execution.

The compiler will add code to save these to local variables before executing the method body; 'old' is supported for strings and value types.

Invariants

In contrast to pre and post conditions, Invariants are used to define a fixed state the object must fulfill at any given time. Invariants can be public or private.

Public invariants will be checked at the end of every public method (after the method's "ensure" block, if present, has been checked) and if an invariant fails, an assertion is raised.

Private invariants will be checked at the end of every method call, public or private.

The idea behind this separation is that public invariants must not be met by private methods, so theoretically a public method can defer work to several private worker methods, and public invariants would only be checked after the public method finishes

Examples:

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

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.

Custom Messages

By default, a generic assertion method is generated. For example, suppose that Method1 failed the following require:

require A > 10;

This would generate the following message: "Method1 assertion failed A > 10".

Custom messages can be generated instead by adding : 'your message' to the require, ensure or invariant statement, e.g.:

method MyObject.Add(aItem: ListItem);
require
  assigned(aItem) : 'List Item for MyObject cannot be nil';
begin
  InternalList.Add(aItem);
ensure
  Count = old Count +1 : 'MyObject: Count logic error';
End;

Remarks

Note that not all elements of a class can be used inside invariants because some elements of a class (or the entire class system of your application) can be accessed and written to directly, without the knowledge of the class.

If, for example, your invariant were to depend on a public field*, other parts of your system would be able to modify this field directly, bypassing the invariant checking.

Elements that can be used in invariants are:

• private fields.
• properties
• methods

* of course non-private fields are discouraged in general and you should always use private fields and - where needed - a property with a higher visibility to make the field accessible.

See Also

• Class Members
• Invariants
• require
• ensure
• old
• Assert (Compiler Magic Function)

• External video about class contracts by Barry Carr: part 1 – part 2

Product: RemObjects Oxygene (formerly known as Chrome)
Current version: 3.0 Previous Versions: 'Joyride' (2.0), 'Floorshow' (1.5), 'Adrenochrome' (1.0)

Glossary — Keywords — Language Features — Platform Features — Samples — Articles — How To — Issues