Specification and Verification of Invariants by Exploiting Layers in OO Designs

• Autorzy: Middelkoop R. , Huizing C. , Kuiper R. , Luit E.J.
• Języki publikacji: EN

Abstrakty

EN

The layering that is present in many OO designs is not accounted for in current interpretations of invariants. We propose to make layers explicit in specifications and introduce a new interpretation of invariants that exploits these layers. Furthermore, we present a sound, modular technique to statically verify that programs satisfy the new interpretation.

Słowa kluczowe

EN

OO designs; interpretation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 377--398
• Opis fizyczny: bibliogr. 30 poz.

Twórcy

autor

Middelkoop R.

autor

Huizing C.

autor

Kuiper R.

autor

Luit E.J.

• Department of Mathematics and Computer Science, Technische Universiteit Eindhoven , P.O.Box 513, 5600 MB Eindhoven, The Netherlands,

Bibliografia

• [1] Barnett, M., DeLine, R., F¨ahndrich, M., Leino, K. R. M., Schulte, W.: Verification of object-oriented programs with invariants, Journal of Object Technology, 3(6), June 2004, 27-56.
• [2] Barnett, M., Leino, K. R. M., Schulte,W.: The Spec# programming system: An overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS '04), LNCS 3362, Springer, 2005.
• [3] Barnett, M., Naumann, D. A.: Friends Need a Bit More: Maintaining Invariants Over Shared State, Mathematics of Program Construction (MPC '04), LNCS 3125, Springer, 2004.
• [4] Baumeister, H., Hennicker, R., Knapp, A., Wirsing, M.: OCL Component Invariants, Monterey Workshop 2001, Engineering Automation for Software Intensive System Integration, Monterey, USA, 2001.
• [5] Booch, G.: Object-Oriented Analysis and Design with Applications, 2nd edition, Benjamin-Cummings, 1994.
• [6] Clarke, D.: Object Ownership and Containment, Ph.D. Thesis, University of New SouthWales, 2001.
• [7] Dietl, W., M¨uller, P.: Universes: Lightweight Ownership for JML, Journal of Object Technology, 4(8), 2005, 5-32.
• [8] Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1995.
• [9] Guttag, J. V., Horning, J. J.: Larch: Languages and Tools for Formal Specification, Springer, 1993.
• [10] Hoare, C. A. R.: Proof of Correctness of Data Representations, Acta Informatica, 1, 1972, 271-281.
• [11] Huizing, K., Kuiper, R.: Verification of Object Oriented Programs Using Class Invariants, Fundamental Approaches to Software Engineering (FASE' 00), LNCS 1783, Springer, 2000.
• [12] Jacobs, B., Smans, J., Piessens, F., Schulte,W.: A Simple Sequential Reasoning Approach for SoundModular Verification of Mainstream Multithreaded Programs, ENTCS, 174(9), 2007, 23-47.
• [13] Kassios, I. T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions, Formal Methods (FM '06), LNCS 4085, Springer, 2006.
• [14] Leavens, G. T., Baker, A. L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java, SIGSOFT Softw. Eng. Notes, 31(3), 2006, 1-38.
• [15] Leino, K. M.: Toward Reliable Modular Programs, Ph.D. Thesis, California Institute of Technology, 1995.
• [16] Leino, K. R. M., M¨uller, P.: Object Invariants in Dynamic Contexts, European Conference on Object- Oriented Programming (ECOOP' 04), LNCS 3086, Springer, 2004.
• [17] Leino, K. R.M.,M¨uller, P.: Modular Verification of Static Class Invariants, FormalMethods (FM'05), LNCS 3582, Springer, 2005.
• [18] Meyer, B.: Object-Oriented Software Construction, Second Edition, Prentice-Hall, 1997.
• [19] Middelkoop, R., Huizing, C., Kuiper, R., Luit, E. J.: Invariants for Non-Hierarchical Object Structures, Brazilian Symposium on Formal Methods (SBMF'06), ENTCS 195, Elsevier, 2008.
• [20] Middelkoop, R., Huizing, C., Kuiper, R., Luit, E. J.: A Proof System for Invariants in Layered OO Designs, Technical report, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, 2008, Available from http://alexandria.tue.nl/repository/books/633066.pdf.
• [21] M¨uller, P.: Modular specification and verification of object oriented programs, LNCS 2262, Springer, 2002.
• [22] M¨uller, P., Poetzsch-Heffter, A., Leavens, G. T.: Modular invariants for layered object structures, Science of Computer Programming, 62(3), 2006, 253-286.
• [23] Parkinson,M.: Local Reasoning for Java, Ph.D. Thesis, University of Cambridge, 2005.
• [24] Parnas, D. L.: On the criteria to be used in decomposing systems into modules, Communications of the ACM, 15(12), 1972, 1053-1058.
• [25] Pierik, C.: Validation techniques for object-oriented proof outlines, Ph.D. Thesis, Universiteit Utrecht, 2006.
• [26] Pierik, C., Clarke, D., de Boer, F. S.: Controlling Object Allocation Using Creation Guards, Formal Methods (FM '05), LNCS 3582, Springer, 2005.
• [27] Poetzsch-Heffter, A.: Specification and Verification of Object-Oriented Programs, Habilitationsschrift, Technische Universität München, 1997.
• [28] Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java, European Symposium on Programming Languages and Systems (ESOP' 99), LNCS 1576, 1999.
• [29] Rumbaugh, J. R., Blaha, M. R., Lorensen, W., Eddy, F., Premerlani, W.: Object-Oriented Modeling and Design, Prentice Hall, 1990.
• [30] Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML, Addison-Wesley, 1999.