Title :
Information Hiding and Visibility in Interface Specifications
Author :
Leavens, Gary T. ; Müller, Peter
Author_Institution :
Iowa State Univ., Ames, IA
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 :
Java; data encapsulation; formal specification; reasoning about programs; software maintenance; Java-like language; information hiding; information visibility; interface specification; non privileged client; program maintenance; program verification; sound modular reasoning; Contracts; Documentation; Formal specifications; Java; Packaging; Protection; Software engineering; Specification languages; Testing; Upper bound;
Conference_Titel :
Software Engineering, 2007. ICSE 2007. 29th International Conference on
Conference_Location :
Minneapolis, MN
Print_ISBN :
0-7695-2828-7
DOI :
10.1109/ICSE.2007.44