Abstract
We define a predicate-transformer semantics for an object- oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility control, dynamic binding, and recursive methods. Using the semantics, we formulate notions of refinement. Such results are a first step towards a refinement calculus.
Chapter PDF
Similar content being viewed by others
References
Pierre America and Frank de Boer. Reasoning about dynamically evolving process structures. Formal Aspects of Computing, 6:269–316, 1994.
Martíin Abadi and K. Rustan Leino. A logic of object-oriented programs. In Proceedings, TAPSOFT 1997. Springer-Verlag, 1997. Expanded in DEC SRC report 161.
R. J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.
Marcello M. Bonsangue, Joost N. Kok, and Kaisa Sere. An approach to object-orientation in action systems. In Johan Jeuring, ed., Mathematics of Program Construction, LNCS 1422, pages 68–95. Springer, 1998.
Paulo Borba. Where are the laws of object-oriented programming? In I Brazilian Workshop on Formal Methods, pages 59–70, Porto Alegre, Brazil, 19th-21st October 1998.
A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for an Object-oriented Language of Refinement-Extended Version. Available at http://www.di.ufpe.br/~alcc
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.
A. L. C. Cavalcanti, A. Sampaio, and J. C. P. Woodcock. An inconsistency in procedures, parameters, and substitution in the refinement calculus. Science of Computer Programming, 33(1):87–96, 1999.
C. A. R. Hoare and J. He. Unifying Theories of Programming. Prentice Hall, 1998.
C. A. R. Hoare and J. He and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2), 1987.
Kevin Lano. Formal Object-Oriented Development. Springer, 1995.
K. Rustan M. Leino. Recursive object types in a logic of object-oriented programming. In Chris Hankin, ed., 7th European Symposium on Programming, LNCS 1381. Springer, 1998.
Barbara H. Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6), 1994.
A. Mikhajlova and E. Sekerinski, Class refinement and interface refinement in object-oriented programs.InProceedings of FME’97: Industrial Benefit of Formal Methods. Springer, 1997.
Carroll Morgan. Programming from Specifications, 2ed. Prentice Hall, 1994.
David A. Naumann. Validity of data re nement for a higher order imperative language. Submitted.
David A. Naumann. Predicate transformer semantics of a higher order imperative language with record subtypes. Science of Computer Programming, 1998. To appear.
U. S. Reddy. Objects and classes in Algol-like languages. In Fifth Intern. Workshop on Foundations of Object-oriented Languages. URL: http://pauillac.inria.fr/ remy/fool/proceedings.html, Jan 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cavalcanti, A., Naumann, D.A. (1999). A weakest precondition semantics for an object-oriented language of refinement. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_26
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive