Modular Enforcement of Supertype Abstraction and Information Hiding With Client-Side Checking
Contemporary run-time assertion checkers for object-oriented languages over-zealously check assertions on the supplier side. For method calls, such supplier-side checking occurs at the exact run-time type of the receiver object, which in general can be a proper subtype of the receiver object's static type. However, the receiver object's static type is used for verification in the supertype abstraction technique that static verification tools employ for modular verification. This difference in types causes an inconsistency between run-time assertion checking and static verification tools.