Tagged Types Substitutability Testing is a way of verifying the Liskov substitution principle (LSP) by testing. LSP is a principle stating that if S is a subtype of T (in Ada, S is a derived type of tagged type T), then objects of type T may be replaced with objects of type S (that is, objects of type S may be substituted for objects of type T), without altering any of the desirable properties of the program. When the properties of the program are expressed in the form of subprogram preconditions and postconditions (let's call them pre and post), LSP is formulated as relations between the pre and post of primitive operations and the pre and post of their derived operations. The pre of a derived operation should not be stronger than the original pre, and the post of the derived operation should not be weaker than the original post. Those relations ensure that verifying if a dispatching call is safe can be done just by using the pre and post of the root operation.
Verifying LSP by testing consists of running all the unit tests associated with the primitives of a given tagged type with objects of its derived types.
In the example used in the previous section, there was clearly a violation of LSP. The overriding primitive Adjust_Speed in package Speed2 removes the functionality of the overridden primitive and thus doesn't respect LSP. Gnattest has a special option to run overridden parent tests against objects of the type which have overriding primitives:
gnattest --harness-dir=driver --liskov -Ptagged_rec.gpr
cd driver
gprbuild -Ptest_driver
test_runner
While all the tests pass by themselves, the parent test for Adjust_Speed fails against objects of the derived type.