I created a new project about experiment on object oriented notion of subclasing/substitutability based on annotations.
You annotate mutator methods, and observer methods.
Mutators act to change object state, observer to inspect object state.
Instance generator is also defined, by annotations, to any mutator, to generate a (repeatable ) sequence of parameters to be applied to the methods.
A "random" computation on class is done involving the class, and is based on a repeatable sequence of instance generated to be applied to mutators methods.
It is repeated a second time, involving the subclass instead of the class. The empirical evidence of substitutability is the fact that at any step of the first and the second computation, there is equivalence, where equivalence is defined by same observable state, defined in terms of observer methods.