Abstract
Simulation is the most widely used technique to prove data refinement. We define forward simulation for a language with recursive classes, inheritance, type casts and tests, dynamic binding, class based visibility, mutable state (without aliasing), and specification constructs from refinement calculi. It is a language based on sequential Java, but it also includes specification and deseign mechanisms appropriate for the construction of programs based on refinement. We show simulation to be sound for data refinement of classes in this language.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Martín Abadi and K. Rustan M. Leino. A logic of object-oriented programs. In Proceedings, TAPSOFT 1997. Springer-Verlag, 1997. Expanded in DEC SRC report 161.
R. J. R. Back. Procedural Abstraction in the Refinement Calculus. Technical report, Department of Computer Science, Åbo-Finland, 1987. Ser. A No. 55.
R. J. R. Back and J. Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.
Anindya Banerjee and David Naumann. Representation independence, confinement and access control. In POPL2002, pages 166–177, 2001.
Martin Büchi and Wolfgang Weck. The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science, August 1999. http://www.abo.fi/~mbuechi/publications/TR297.html.
A. L. C. Cavalcanti and D. Naumann. A Weakest Precondition Semantics for an Object-oriented Language of Refinement. In J. M. Wing, J. C. P. Woodcock, and J. Davies, editors, FM’99: World Congress on Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1439–1459. Springer-Verlag, September 1999.
A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for Refinement of Object-oriented Programs. IEEE Transactions on Software Engineering, 26(8):713–728, August 2000.
A. L. C. Cavalcanti and D. A. Naumann. Forward Simulation for Data Refinement of Classes-Extended Version. Technical Report 2001-4, Computer Science, Stevens Institute of Technology, 2001. http://www.cs.stevens-tech.edu/~naumann/tr2001-4.ps.
A. L. C. Cavalcanti and David A. Naumann. On a specification-oriented model for object-orientation. In Proceedings of the VI Brazilian Symposium on Programming Languares, 2002. To appear.
A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society, 5(1):1–15, 1998.
Willem-Paul de Roever and Kai Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998.
David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Technical Report Report 159, Compaq Systems Research Center, December 1998.
Martin Fowler. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 1999.
P. H. B. Gardiner and C. C. Morgan. Data Refinement of Predicate Transformers. Theoretical Computer Science, 87:143–162, 1991.
J. He, C. A. R. Hoare, and J. W. Sanders. Prespecification in Data Refinement. Information Processing Letters, 25(1), 1987.
C. A. R. Hoare. Proof of Correctness of Data Representations. Acta Informatica, 1:271–281, 1972.
C. A. R. Hoare, J. He, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701–739, 1993.
Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion language for mutable data structures. In POPL. ACM Press, 2001.
C. B. Jones. Software Development: A Rigorous Approach. Prentice-Hall, 1980.
G. T. Leavens and W. E. Weihl. Specification and verification of object-oriented programas using supertype abstraction. Acta Informatica, 32, 1995.
Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA 2000 Companion, Minneapolis, Minnesota, pages 105–106. ACM, October 2000.
Gary T. Leavens and Don Pigozzi. A complete algebraic characterization of behavioral subtyping. Acta Informatica, 36:617–663, 2000.
K.R.M Leino, A. Poetzsch-Heffter, and Y. Zhou. Using data groups to specify and check side effects. In Programming Language Design and Implementation 2002, 2002. To appear.
B. H. Liskov and J. M. Wing. A Behavioural Notion of Subtyping. ACM Transactions on Programming Languages and Systems, 16(6), 1994.
Nancy Lynch and Frits Vaandrager. Forward and backward simulations part I: Untimed systems. Information and Computation, 121(2), 1995.
C. C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994.
C. C. Morgan and P. H. B. Gardiner. Data Refinement by Calculation. Acta Informatica, 27(6):481–503, 1990.
P. Müller. Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversität Hagen, 2001. Available from http://www.informatik.fernuni-hagen.de/pi5/publications.html.
David A. Naumann. Soundness of data refinement for a higher order imperative language. Theoretical Computer Science, 278(1–2):271–301, 2002.
Gordon Plotkin. Lambda definability and logical relations. Technical Report SAI-RM-4, University of Edinburgh, School of Artificial Intelligence, 1973.
A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S. D. Swierstra, editor, Programming Languages and Systems (ESOP’ 99), volume 1576 of Lecture Notes in Computer Science, pages 162–176. Springer-Verlag, 1999.
John Power and Edmund Robinson. Logical relations and data abstraction. In Computer Science Logic, 2000.
U. S. Reddy. Objects and classes in Algol-like languages. In Fifth Intern. Workshop on Foundations of Object-oriented Languages, Jan 1998. Full version to appear in Information and Computation.
John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millenial Perspectives in Computer Science. Palgrave, 2001.
Clemens Szyperski. Component Software: Beyond Object-Oriented Programming. ACM Press Books. Addison-Wesley, 1999.
R. D. Tennent. Correctness of data representations in Algol-like languages. In A. W. Roscoe, editor, A Classical Mind: Essays Dedicated to C A. R. Hoare. Prentice-Hall, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cavalcanti, A., Naumann, D.A. (2002). Forward Simulation for Data Refinement of Classes. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_27
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive