Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front Comput Sci Chin    2011, Vol. 5 Issue (3) : 341-352    https://doi.org/10.1007/s11704-011-0130-y
RESEARCH ARTICLE
Pre-post notation is questionable in effectively specifying operations of object-oriented systems
Shaoying LIU()
Department of Computer Science, Hosei University, Tokyo184–8584, Japan
 Download: PDF(207 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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
 Cite this article:   
Shaoying LIU. Pre-post notation is questionable in effectively specifying operations of object-oriented systems[J]. Front Comput Sci Chin, 2011, 5(3): 341-352.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-011-0130-y
https://academic.hep.com.cn/fcs/EN/Y2011/V5/I3/341
Fig.1  Specification of class A
Fig.2  Speci.cation of anotherClass1
Fig.3  Another possible specification for class A
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
[1] Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[2] ZHANG Jian, ZHANG Wenhui, ZHAN Naijun, SHEN Yidong, CHEN Haiming, ZHANG Yunquan, WANG Yongji, WU Enhua, WANG Hongan, ZHU Xueyang. Basic research in computer science and software engineering at SKLCS[J]. Front. Comput. Sci., 2008, 2(1): 1-11.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed