Modular Enforcement of Supertype Abstraction and Information Hiding
		      with Client-Side Checking
				  by
	  Henrique Rebelo, Gary T. Leavens, and Ricardo Lima

			       Abstract

Static reasoning tools for object-oriented (OO) languages use
supertype abstraction, by verifying calls to methods using the
specification associated with the receiver's static type.
Unfortunately, contemporary runtime assertion checkers for OO are
inconsistent with such static reasoning tools, since they check
assertions in an overly-dynamic way on the supplier side.  For method
calls, such supplier-side checking occurs at the exact runtime type of
the receiver object, which in general can be a proper subtype of the
receiver object's static type.  Since such a subtype can have a
refinement of the corresponding supertype's specification, this
specification difference can cause an inconsistency between runtime
assertion checking and static verification tools.  We explain how our
technique of client-side checking allows runtime assertion checkers to
use the specifications associated with static types, gaining
consistency with static verification tools.  Another advantage of such
client-side checking is that it provides a way for runtime assertion
checkers to use privacy information associated with specifications,
which promotes information hiding.

Keywords: Object-oriented programming; Runtime assertion checking; Modularity;
Modular reasoning; Supertype abstraction; Information Hiding.

2011 CR Categories:
D.2.1 [Software Engineering]
        Requirements/ Specifications --- languages, tools, JML;
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers,
                class invariants, formal methods, programming by contract,
                reliability, tools, validation, JML;
D.2.5 [Software Engineering]
        Testing and Debugging --- Debugging aids, design,
                testing tools, theory;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, pre- and post-conditions,
                specification techniques.