This Article 
 Bibliographic References 
 Add to: 
A Weakest Precondition Semantics for Refinement of Object-Oriented Programs
August 2000 (vol. 26 no. 8)
pp. 713-728

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 toward a refinement calculus.

[1] M. Abadi and L. Cardelli, A Theory of Objects. 1996.
[2] D. Aspinall and A. Compagnoni, “Subtyping Dependent Types,” Proc. 11th IEEE Symp. Logic in Computer Science, 1996.
[3] P. America and F. de Boer, “Reasoning About Dynamically Evolving Process Structures,” Formal Aspects of Computing, vol. 6 pp. 269–316, 1994.
[4] Formal Syntax and Semantics of Java. J. Alves-Fossed ed., 1999.
[5] M. Abadi and K.R.M. Leino, “A Logic of Object-Oriented Programs,” Proc. Theory and Practice of Software Development, 1997.
[6] R.J.R. Back, “Procedural Abstraction in the Refinement Calculus,” technical report, Computer Science Dept.,Åbo, Finland, 1987.
[7] M.M. Bonsangue, J.N. Kok, and K. Sere, “An Approach to Object-Orientation in Action Systems,” Math. of Program Construction, Johan Jeuring, ed., vol. 1422, pp. 68–95, 1998.
[8] R.J.R. Back, A. Mikhajlova, and J. von Wright, “Class Refinement as Semantics of Correct Object Substitutability,” technical report , Turku Center for Computer Science, Dec. 1997.
[9] P.H.M. Borba, “Where Are the Laws of Object-Oriented Programming?” Proc. Brazilian Workshop Formal Methods, pp. 59–70, Oct. 1998.
[10] R.J.R. Back and J. von Wright, Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.
[11] A.L.C. Cavalcanti and D.A. Naumann, “A Weakest Precondition Semantics for an Object-Oriented Language of Refinement,” Proc. FM '99: World Congress on Formal Methods, J.M. Wing, J.C.P. Woodcock, and J. Davies, eds., pp. 1439–1459, Sept. 1999.
[12] A.L.C. Cavalcanti and D.A. Naumann, “A Weakest Precondition Semantics for an Object-Oriented Language of Refinement-Extended Version,” Technical Report CS 9903, Stevens Inst. of Tech nology, Sept. 1999. .
[13] A.L.C. Cavalcanti, A.C.A. Sampaio, and J.C.P. Woodcock, “Procedures and Recursion in the Refinement Calculus,” J. Brazilian Computer Soc., vol. 5, no. 1, pp. 1–15, 1998.
[14] 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, vol. 33, no. 1, pp. 87–96, 1999.
[15] A.L.C. Cavalcanti and J.C.P. Woodcock, “A Weakest Precondition Semantics for Z,” The Computer J., vol. 41, no. 1, pp. 1–15, 1998.
[16] A.L.C. Cavalcanti and J.C.P. Woodcock, “ZRC - A Refinement Calculus for Z,” Formal Aspects of Computing, vol. 10, no. 3, pp. 267–289, 1999.
[17] P.H.B. Gardiner and C.C. Morgan, “A Single Complete Rule for Data Refinement,” Formal Aspects of Computing, vol. 5, no. 4, pp. 367–382, 1993.
[18] D. Gries, The Science of Programming.New York, Heidelberg, Berlin: Springer-Verlag, 1981.
[19] J. He, C.A.R. Hoare, and J.W. Sanders, “Data Refinement Refined,” Proc. ESOP'86 European Symp. Programming, G. Goos and H. Hartmants, eds., pp. 187–196, Mar. 1986.
[20] J. He, C.A.R. Hoare, and J.W. Sanders, “Prespecification in Data Refinement,” Information Processing Letters, vol. 25, no. 1, 1987.
[21] K. Lano, Formal Object-Oriented Development. 1995.
[22] K.R.M. Leino, “Recursive Object Types in a Logic of Object-Oriented Programming,” Proc. Seventh European Symposium on Programming, C. Hankin, ed., 1998.
[23] Object-Oriented Specification Case Studies, K. Lano and H. Haughton, eds., 1994.
[24] K.R.M. Leino and R. Manohar, “Joining Specification Statements,” Theoretical Computer Science, 1998.
[25] B. Liskov and J.M. Wing, ”A Behavioral Notion of Subtyping,” ACM Trans. Programming Languages and Systems, vol. 16, no. 6, pp. 1,811–1,841, Nov. 1994.
[26] C.C. Morgan, Programming from Specifications, second edition. Englewood Cliffs, N.J.: Prentice Hall, 1994.
[27] A. Mikhajlova and E. Sekerinski, “Class Refinement and Interface Refinement in Object-Oriented Programs,” Proc. Formal Methods Europe: Industrial Benefit of Formal Methods, 1997.
[28] L. Mikhajlov and E. Sekerinski, “A Study of the Fragile Base Class Problem,” Proc. European Conf. Object-Oriented Programming, E. Jul, ed., 1998.
[29] C.C. Morgan and T.N. Vickers, On the Refinement Calculus. Springer-Verlag, 1994.
[30] D.A. Naumann, “Predicate Transformer Semantics of a Higher Order Imperative Language with Record Subtypes,” to be publishied in Science of Computer Programming, 2000.
[31] D.A. Naumann, “Soundness of Data Refinement for a Higher Order Imperative Language,” to be published in Theoretical Computer Science, 2000.
[32] U.S. Reddy, “Objects and Classes in Algol-Like Languages,” Proc. Fifth Int'l Workshop Foundations of Object-Oriented Languages, Jan. 1998. .
[33] Object-Orientation in Z, S. Stepney, R. Barden and D. Cooper eds. Springer-Verlag, 1992.
[34] M. Utting and K. Robinson, “Modular Reasoning in an Object-Oriented Refinement Calculus,” Proc. Second Int'l Conf. Mathematics of Program Construction, R.S. Bird, C.C. Morgan, and J.C.P. Woodcock, eds., pp. 344–367, 1993.

Index Terms:
Refinement calculi, semantic models, object-orientation, verification.
Ana Cavalcanti, David A. Naumann, "A Weakest Precondition Semantics for Refinement of Object-Oriented Programs," IEEE Transactions on Software Engineering, vol. 26, no. 8, pp. 713-728, Aug. 2000, doi:10.1109/32.879810
Usage of this product signifies your acceptance of the Terms of Use.