A formal bridge between runtime assertion checking and static verification of inheritance

Resumen

In object-oriented programming languages, the
relationship that should hold between the specifications
of a class and its superclass is called behavioural
subtyping. In this paper we analyse the conditions that
a behavioural subtype should meet during runtime
assertion checking, that is, during dynamic verification.
Our exploration relates such conditions for runtime
assertion checking to the conditions that should be
met in static verification of correctness under the
principles of modular reasoning. As a result, we state
and prove a theorem that connects dynamic and
static verification of method calls in the presence of
inheritance. The novelty of this theorem lies on the
fact that the connection is an equivalence, where the
implication from static to dynamic verification has been
explored before but not the opposite one. This new
exploration then poses that a hypothetical exhaustive
testing through runtime assertion checking would be
equivalent to the corresponding static verification of
definite correctness, which adds solidity to runtime
assertion checking. None but one of the runtime
assertion checking tools that we know of can effectively
detect all possible problems in class inheritance; the one
exception is the tool used for Spec#, but their strategy
relies on both specification inheritance and a rather
substantial restriction on preconditions, requirements we
could dispose of when taking our the-oretical results to
a practical implementation.