Leavens, Gary T. and Müller, Peter (2006) Information Hiding and Visibility in Interface Specifications. Technical Report 06-28, Computer Science, Iowa State University.
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.|
|Subjects:||Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)|
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
|Deposited by:||Gary T. Leavens on 11 September 2006|
|Alternative Locations:||ftp://ftp.cs.iastate.edu/pub/techreports/TR06-28/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR06-28/TR.ps.gz |
Contact site administrator at: email@example.com