High-integrity object-oriented programming with Ada - Part 1

Three Approaches
The new guidance³ addresses this issue by defining a new concept, local type consistency verification, which ensures that class hierarchies sufficiently conform to LSP to address the vulnerability. The “local” in local type consistency refers to the fact that consistency verification can be limited to the cases that actually occur in the application. There are three approaches:

1) Formally verify substitutability; i.e., demonstrate two properties:

• The preconditions for the subclass’s version of the operation are no stronger than those in the superclass;

• The post conditions for the subclass’s version of the operation are no weaker than those in the superclass.

Although at first glance these may seem counterintuitive — specialization seems to imply the strengthening of preconditions — in fact they follow directly from the semantics of dynamic dispatch. The context of a dynamically dispatching call can only be assumed to know the pre- and post conditions for the operation as defined for the root of the inheritance hierarchy, since some of the potential subclasses might not even be written yet. If a subclass’s version of the operation strengthens the preconditions, then the call may fail because it has been written assuming the weaker preconditions and could not have anticipated new constraints such as those expressed in a strengthened precondition. An analogous situation holds with respect to post conditions.

For instance, with the formal verification approach, if an operation is never invoked through dynamic dispatch, there is no need to verify that its precondition is no stronger than its superclass’s version. This approach offers a direct verification of LSP. It is the recommended path when appropriate formal methods can be used, since they provide the highest level of confidence.

2) Ensure that each subclass passes all the tests of all its superclasses that it can replace. The second approach is well suited to verification based on unit testing. In such a context, each operation in a class is associated with a set of tests that verify its requirements. An overridden operation usually has extended requirements compared to the operation it overrides, so it will be associated with an extended set of tests. Each class can be tested separately by calling the tests of its operations. In order to use testing to verify substitutability of a given class by one of its subclasses, run all the tests for all superclasses with objects of the given subclass. If all the superclass tests pass, this provides a high degree of confidence that objects of the subclass can properly substitute for superclass objects.

3) For each dispatch point, perform pessimistic testing; i.e., test every operation that can be invoked. Pessimistic testing, may be the simplest verification method when dispatching calls are rare and the class hierarchy is shallow and/or narrow.

The developer’s approach to local type consistency verification depends on the language technology and how dynamic dispatch is used in the application. For example, formal verification is possible with some languages but not with others. In simple situations, pessimistic testing may be practical.

Static binding versus dynamic dispatch
Object oriented languages typically use the syntax v.Op(…) to indicate an operation Op applied to a polymorphic variable v. In some situations (static binding) the appropriate version of Op is identified based on the compile-time type specified in the declaration of v. In other cases (dynamic dispatch) the operation is identified based on the run-time type (class) of the object that v. denotes. If it is not clear which rule applies, this compromises readability/understandability, introducing another potential vulnerability.