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

doi:10.1007/s11704-011-0130-y

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