Contract inheritance for interfaces and classes
Interface and class member functions can also have
out blocks. This allows an interface or a class to define preconditions for its derived types to depend on, as well as to define postconditions for its users to depend on. Derived types can define further
out blocks for the overrides of those member functions. Overridden
in blocks can loosen preconditions and overridden out blocks can offer more guarantees.
User code is commonly abstracted away from the derived types, written in a way to satisfy the preconditions of the topmost type in a hierarchy. The user code does not even know about the derived types. Since user code would be written for the contracts of an interface, it would not be acceptable for a derived type to put stricter preconditions on an overridden member function. However, the preconditions of a derived type can be more permissive than the preconditions of its superclass.
Upon entering a function, the
in blocks are executed automatically from the topmost type to the bottom-most type in the hierarchy. If any
in block succeeds without an
assert failure, then the preconditions are considered to be fulfilled.
Similarly, derived types can define
out blocks. Since postconditions are about the guarantees that a function provides, the member functions of the derived type must observe the postconditions of its ancestors as well. On the other hand, it can provide additional guarantees.
Upon exiting a function, the
out blocks are executed automatically from the topmost type to the bottom-most type. The function is considered to have fulfilled its postconditions only if all of the
out blocks succeed.
The following artificial program demonstrates these features on an interface and a class. The class requires less from its callers while providing more guarantees: