Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known statically: this is the well-known feature of dispatching calls, a.k.a. late binding, whereby the target of the call depends on the dynamic type of the object on which it's called. For example, the standard for civil avionics certification has recognized this specific problem, and defines a specific verification objective called Local Type Consistency that should be met with one of three strategies (DO-332 document, paragraph OO.6.7.2):

1. Verify substitutability using formal methods.
2. Ensure that each class passes all the tests of all its parent types which the class can replace.
3. For each call point, test every method that can be invoked at that call point (pessimistic testing).

SPARK allows using strategy 1 above, by defining the behavior of an overridden subprogram using a class-wide contract (introduced by aspects Pre'Class and Post'Class) and checking that the behavior of the overriding subprogram (also defined using a class-wide contract) is a suitable substitution. What is a suitable substitution? One that satisfies the Liskov Substitution Principle (a.k.a. LSP, named after Barbara Liskov who defined it in an article with Jeannette Wing in 1993), which essentially says that the behaviors of the overriding subprogram are a subset of the possible behaviors of the overridden subprogram. When programming by contract is used, as in SPARK, this translates as two essential properties:

1. The precondition of the overriding subprogram should be equal or less restrictive than the precondition of the overridden subprogram.
2. The postcondition of the overriding subprogram should be equal or give more guarantees than the postcondition of the overridden subprogram.

For example, assume that you have a tagged type Object that defines a procedure Draw to display the object on screen. The Draw procedure may require that the object is fully visible, and may set a flag in the object to record that it has been drawn:

Then, Object may be derived in a number of specific objects, say a box, which define their own Draw procedure. In order to respect LSP, these new procedures should have preconditions that can only weaken the precondition on Object, and postconditions that can only strengthen the postcondition on Object. For example, here is an overriding of Draw that respects LSP:

Assuming that a box always occupies some space, if it is included in the screen then its intersection with the screen is not empty, hence the precondition of the overriding subprogram is indeed weaker than the precondition of the overridden one. For the postcondition, the one of the overriding subprogram is the same as the one of the overridden subprogram, plus an additional property, hence it is stronger.

An overriding of Draw that does not respect LSP could either fail to keep or weaken its precondition:

or fail to keep or strengthen its postcondition:

GNATprove can be used to check automatically that overriding subprograms respect LSP, and will detect the bad overridings above. The benefit of enforcing LSP is that the same class-wide contract can be used to analyze calls to all possible targets of a dispatching call. Thus, proof of code with dispatching calls is no more complex than proof of code with regular calls, except the class-wide contract is used for dispatching calls instead of regular contracts for regular calls.

For more details on how Object Oriented programs can be verified with GNATprove, see the SPARK User's Guide.