Pre-post notation is questionable in effectively specifying operations of object-oriented systems

Abstract

There is a growing tendency for people in the community of object-oriented methods to use pre- and post-conditions to write formal specifications for operations (methods) of classes. The motivation for trying to take advantage of well established formalism in precisely defining the functionality of operations is laudable, but unfortunately this exercise may be flawed because the use of pre- and post-conditions containing method calls (or similar) with side effects are likely to cause confusion in the interpretation of specifications. This paper analyzes, with comprehensible examples, why using pre-post notation is not effective to specify operations in object-oriented systems in general, discusses existing approaches to using pre-post notation for object-oriented systems, and offers some solutions to the problem.

Keywords

formal specification / object-oriented systems / software development

References

[1] Jones C B. Systematic Software Development Using VDM. 2nd ed. Upper Saddle River: Prentice Hall, 1990

[2] Woodcock J, Davies J. Using Z: Specification, Refinement, and Proof. Upper Saddle River: Prentice Hall, 1996

[3] Abrial J R. The B-Book: Assigning Programs to Meanings. New York: Cambridge University Press, 1996

[4] Liu S. Formal Engineering for Industrial Software Development Using the SOFL Method. Heidelberg: Springer, 2004.

[5] Liu S, Offutt A J, Ho-Stuart C, Sun Y, Ohba M. SOFL: a formal engineering methodology for industrial applications. IEEE Transactions on Software Engineering, 1998, 24(1): 24–45

[6] Hoare C A R, Wirth N. An axiomatic definition of the programming language PASCAL. Acta Informatica, 1973, 2(4): 335–355

[7] Smith G. The Object-Z Specification Language. Norwell: Kluwer Academic Publishers, 2000

[8] Meyer B. Object-Oriented Software Construction. Upper Saddle River: Prentice Hall, 1997

[9] Warmer J, Kleppe A. The Object Constraint Language: Getting Your Models Ready for MDA. Boston: Addison-Wesley, 2003

[10] Filipe J K, Lau K K, Ornaghi M, Taguchi K, Yatsu H, Wills A. Formal specification of catalysis frameworks. In: Proceedings of 7th Asia-Pacific Software Engineering Conference. 2000, 180–187

[11] Fitzgerald J S, Larsen P G, Mukherjee P, Plat N, Verhoef M. Validated Designs for Object-oriented Systems. Santa Clara: Springer-Verlag, 2005

[12] Bekbay S, Liu S. A study of Japanese software process practices and a potential for improvement using SOFL. In: Proceedings of 3rd International Conference on Quality Software, 2003, 100–1007

[13] Utting M. An object-oriented refinement calculus with modular reasoning, Dissertation for the Doctoral Degree. Sydney: University of New South Wales, Australia, 1992

[14] Utting M, Robinson K. Modular reasoning in an object-oriented refinement calculus. In: Proceedings of 2nd International Conference on Mathematics of Program Construction. 1992, 344–367

[15] Back R J, Mikhajlova A, von Wright J. Class refinement as semantics of correct object substitutability. Journal of Formal Aspects of Computing, 2000, 12(1): 18–40

[16] Cavalcanti A, Naumann D A. Forward simulation for data refinement of classes. In: Proceedings of 2002 International Symposium of Formal Methods. 2002, 471–490

[17] Grithiths A. An extended semantic foundation for Object-Z. In: Proceedings of 3rd Asia-Pacific Software Engineering Conference. 1996, 194–207

[18] Morgan C. Programming From Specifications. Upper Saddle River: Prentice Hall, 1990

[19] Cavalcanti A, Naumann D. A weakest precondition semantics for refinement of object-oriented programs. IEEE Transactions on Software Engineering, 2000, 26(8): 713–728

[20] Meyer B. Eiffel: The Language. Upper Saddle River: Prentice Hall, 1991

[21] Barnett M, DeLine R, Fähndrich M, Leino K R M, Schulte W.Verification of object-oriented programs with invariants. Journal of Object Technology, 2004, 3(6): 27–56

[22] Leavens G T, Cheon Y. Design by contract with JML. ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmldbc.pdf.

[23] Duan Z, Tian C. A unified model checking approach with projection temporal logic. In: Proceedings of 2008 International Conference on Formal Engineering Methods. 2008, 167–186

[24] Duan Z, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008, 45(1): 43–78

[25] Liu S, Nakajima S. A decompositional approach to automatic test case generation based on formal specifications. In: Proceedings of 4th IEEE International Conference on Secure Software Integration and Reliability Improvement. 2010, 147–155

Acknowledgements

This work was supported by the National Institute of Informatics Collaborative Research Program. It was also supported by the National Natural Science Foundation of China (Grant No. 60910004), and the Major State Basic Research Development Program of China (2010CB328102).

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg