Information Hiding and Visibility in Interface Specifications
                                  by
		  Gary T. Leavens and Peter Mueller

			       Abstract

Information hiding controls which parts of a class are visible to
non-privileged and privileged clients (e.g., subclasses).  This
affects detailed design specifications in two ways.  First,
specifications should not expose hidden class members.  As noted in
previous work, this is important because such hidden members are not
meaningful to all clients.  But it also allows changes to hidden
implementation details without invalidating correctness proofs for
client code, which is important for maintaining verified programs.
Second, to enable sound modular reasoning, certain specifications must
be visible to clients.  We present rules for information hiding in
specifications for Java-like languages, and demonstrate their
application to the specification language JML. These rules restrict
proof obligations to only mention visible class members, but retain
soundness. This allows maintenance of implementations and their
specifications without affecting client reasoning.

Keywords: Information hiding, visibility,
behavioral interface specification language,
proof obligation, public, protected, private, client,
JML language.

2006 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- Languages;
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers, class invariants,
        correctness proofs, formal methods,
        programming by contract, reliability, tools, Spec#, Eiffel, JML;
D.3.3 [Programming Languages]
	Language Constructs and Features --- Modules, Packages;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, logics of programs,
                pre- and post-conditions,
                specification techniques.