Contract Inheritance

Contract inheritance for interfaces and classes

Interface and class member functions can also have in and 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 in and 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: