|
|
Pre-post notation is questionable in effectively specifying operations of object-oriented systems |
Shaoying LIU( ) |
Department of Computer Science, Hosei University, Tokyo184–8584, Japan |
|
|
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
|
Corresponding Author(s):
LIU Shaoying,Email:sliu@hosei.ac.jp
|
Issue Date: 05 September 2011
|
|
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 doi: 10.1017/CBO9780511624162
|
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 doi: 10.1007/BF00289504
|
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 doi: 10.1109/QSIC.2003.1319091
|
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 doi: 10.1007/s001650070034
|
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 doi: 10.1109/APSEC.1996.566754
|
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 doi: 10.1109/32.879810
|
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 doi: 10.5381/jot.2004.3.6.a2
|
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 doi: 10.1007/s00236-007-0062-z
|
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 doi: 10.1109/SSIRI.2010.11
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|