Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Modular Enforcement of Supertype Abstraction and Information Hiding with Client-Side Checking by Henrique Rebelo, Gary T. Leavens, and Ricardo Lima Abstract Contemporary runtime 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 runtime 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 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.