Class Contracts

Class Contracts cover two constructs that enable Design by Contract-like syntax to create classes that can test themselves.

Pre-conditions and Post-conditions
Invariants

If a contract is not upheld, an assertion is generated in the same fashion as calling the assert() system function would.

While originally devised for the Oxygene language, class contracts are available for all Elements languages (except Go, which does not support classes), as language extensions.

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 (Oxygene) or __require and __ensure (C#, Swift and Java) keywords will expand the method body to list the preconditions; both sections can contain a list of Boolean statements, separated by semicolons.

In Oxygene, the require and ensure sections live before and after the main begin/end pair of the method body; in C#, Swift, and Java, __require and __ensure can provided as sub-sections within the body.

Examples:

method MyObject.DivideBy(aValue: Integer);
require
  aValue ≠ 0 : "Cannot divide by zero";
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: Integer);
require
  assigned(fMyWorker);
  fMyValue > 0;
  aValue > 0;
begin
  //... do the work here
ensure
  assigned(fMyResult);
  fMyResult.Value >= 5;
end;

void DivideBy(int value)
{
    __require
    {
        value != 0 : "Cannot divide by zero";
    }
    MyValue = MyValue/value;
}

void Add(ListItem item)
{
    __require
    {
        item != null;
    }
    InternalList.Add(item);
    __ensure
    {
        Count == (__old.Count) + 1;
    }
}

void DoWork(int value)
{
    __require
    {
        fMyWorker != null;
        fMyValue > 0;
        value > 0;
    }
    //... do the work here
    __ensure
    {
        fMyResult != null;
        fMyResult.Value >= 5;
    }
}

func Divide(by value: Integer) {
    __require {
        value != 0 : "Cannot divide by zero";
    }
    MyValue = MyValue/value;
}

func Add(item: ListItem) {
    InternalList.Add(item);
    __ensure {
        Count == (__old.Count) + 1;
    }
}

func DoWork(_ value: Int) {
    __require {
        fMyWorker != null;
        fMyValue > 0;
        value > 0;
    }
    //... do the work here
    __ensure {
        fMyResult != nil;
        fMyResult.Value >= 5;
    }
}

void DivideBy(int value) {
    __require {
        value != 0 : "Cannot divide by zero";
    }
    MyValue = MyValue/value;
}

void Add(ListItem item) {
    __require {
        item != null;
    }
    InternalList.Add(item);
    __ensure {
        Count == (__old.Count) + 1;
    }
}

void DoWork(int value) {
    __require {
        fMyWorker != null;
        fMyValue > 0;
        value > 0;
    }
    //... do the work here
    __ensure {
        fMyResult != null;
        fMyResult.Value >= 5;
    }
}

Sub DivideBy(aValue As Integer)
  Require
    Check aValue ≠ 0, "Cannot divide by zero"
  End Require
  MyValue := MyValue/aValue;
End Sub

Sub Add(aItem As ListItem)
  Require
    Check assigned(aItem)
  End Require
  InternalList.Add(aItem);
  Ensure
    Check Count = (Old.Count) + 1
  End Ensure
End Sub

Sub DoWork(aValue As Integer)
  Require
    Check assigned(fMyWorker)
    Check fMyValue > 0
    Check aValue > 0
  End Require
  ' ... do the work here
  Ensure
    Check assigned(fMyResult)
    Check fMyResult.Value >= 5
  End Ensure
End Sub

The old (Oxygene and Mercury) or __old (C#, Swift and Java) prefix operator can be used in the ensure section for local variables, parameters and properties 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/__old is supported for strings and value types. When used with Reference Types such as Classes, it will capture the old pointer, not the old state of the object being pointed to.

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 marked 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;

public class MyClass
{
    public __invariants
    {
        field1 > 35;
        SomeProperty = 0;
        SomeBoolMethod() && !(fField2 == 5);
    }
    private __invariants
    {
        field > 0;
    }
}

public class MyClass {
    public __invariants {
        field1 > 35
        SomeProperty = 0
        SomeBoolMethod() && !(fField2 == 5)
    }
    private __invariants {
        field > 0
    }
}

public class MyClass {
    public __invariants {
        field1 > 35;
        SomeProperty = 0;
        SomeBoolMethod() && !(fField2 == 5);
    }
    private __invariants {
        field > 0;
    }
}

Public Class MyClass
  '  ... some methods or properties
  Public Invariants
    Check fField1 > 35
    Check SomeProperty = 0
    Check SomeBoolMethod() And Not (fField2 = 5)
  End Invariants
  Private Invariants
    Check fField > 0
  End Invariants
End Class

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 call is generated, using the textual representation of the condition as message. For example, suppose that Method1 failed the following requirement:

require 
  A > 10;

__require
{
    A > 10;
}

__require {
    A > 10
}

__require {
    A > 10;
}

Require
  Check A > 10
End Require

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

Both Invariants and Pre-/Post-Conditions 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 (all languages except Mercury) or a comma (Mercury). If the expression itself contains a colon/comma, the whole expression needs to be wrapped in parenthesis:

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;

void Add(ListItem item)
{
    __require
    {
        (item != null) : "List Item for MyObject cannot be null";
    }
    InternalList.Add(aItem);
    __ensure
    {
        Count == (__old.Count) + 1 : "MyObject: Count logic error";
    }
}

func Add(aItem: ListItem) {
    InternalList.Add(aItem);
    __ensure {
        Count == (__old.Count) + 1 : "MyObject: Count logic error"
    }
}

void Add(ListItem item) {
    __require {
        (item != null) : "List Item for MyObject cannot be null";
    }
    InternalList.Add(aItem);
    __ensure {
        Count == (__old.Count) + 1 : "MyObject: Count logic error";
    }
}

Sub Add(aItem As ListItem)
  Require
    Check assigned(aItem), "List Item for MyObject cannot be nil";
  End Require
  InternalList.Add(aItem);
  Ensure
    Count = Old.Count + 1, "MyObject: Count logic error";
  End Ensure`
End Sub

Notes

Note that not all members 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. Of course non-private fields are discouraged in general and you should always use private fields and – where applicable – a property with a higher visibility to make the field's value accessible.

Members that can be used in invariants are:

private fields
properties
methods

Class Contracts

Pre-Conditions and Post-Conditions

Invariants

Custom Messages

Notes

See Also