Assertions

One of the distinctive features of Freya is the support for contract oriented metodology, through the use of assertions: preconditions, postconditions and class invariants.

Why do we need assertions?

Consider a typical stack declaration:

Stack = class[X]
    // ...
public
    method Push(Value: X);
    method Pop: X;
    property Top: X; readonly;
    property IsEmpty: Boolean; readonly;
end;

• Neither Pop nor Top can be used, unless IsEmpty returns false.
• After calling Push, the stack becomes not empty.

How would you inform these conditions holds to the potential users of this class? There are two common ways: stuffing free form comments here and there, or pushing that information to the software documentation... assuming it will be ever written.

Preconditions

As we said before, we have conditions that must met before calling some executable members, like this one:

• Neither Pop nor Top can be used, unless IsEmpty returns false.

This kind of conditions can be written as preconditions, and they can be associated to any executable member, except static constructors, destructors and events. They are always written along the member declaration, instead than with its implementation:

Stack = class[X]
    // ...
public
    // ...

    method Pop: X;
        requires not Empty;
    property Top: X; readonly;
        requires not Empty;

    property IsEmpty: Boolean; readonly;
end;

A precondition must evaluate as a boolean expression, and may include input parameters and reference parameters from the method it belongs. A precondition attached to an instance member may call any other instance or static member from the declaring class and from any other type, and preconditions attached to an static member may call any other static member from the declaring class or any other type.

Postconditions

• After calling Push, the stack becomes not empty.

Stack = class[X]
    // ...
public
    method Push(Value: X);
        ensures not IsEmpty;
    // ...

    property IsEmpty: Boolean; readonly;
end;

Actually, we can say more about the state of an instance after Push is called:

method Push(Value: X);
    ensures not IsEmpty, Top.Equals(Value);

That is, after a Push operation, the value on the top of the stack is the most recently pushed value.

Customizing the error message

If you don't provide a message for the exception raised when an assertion fails, the compiler will automatically generate a simple message. However, you can include your own message with the assertion:

Stack = class[X]
    // ...
public
    method Push(Value: X);
        ensures not IsEmpty
            raise 'Pushed value not on top';
    // ...

    property IsEmpty: Boolean; readonly;
end;

See also

The Freya Programming Language
Program and file structure
Type declarations
Type members
Statements
Expressions