A formal software development approach based on COOZ and refinement calculus

Author

Yunfeng, Wang ; Bixin, Li ; Jun, Pang ; Ming, Zha ; Guoliang, Zheng

Author_Institution

Nat. Key Lab. for Novel Software Technol., Nanjing Univ., China

fYear

1999

fDate

1999

Firstpage

261

Lastpage

266

Abstract

Including refinement calculus into COOZ complements its disadvantage during design and implementation. The separation between design and implementation for construct and notation is removed as well. Then the software can be developed smoothly in the same frame. There is no corresponding object oriented construct in existing refinement calculus. The combination of COOZ and refinement calculus can build an object oriented frame in which the specification in COOZ is refined stepwise to code by calculus. Two development models are discussed which are based mainly on COOZ and the refinement calculus respectively. The first model is first discussed and then the data refinement and operation refinement is analyzed by example. The two methods of operation refinement for OO formal specification are outlined, and the frame transition rule from COOZ to C++ is examined

Keywords

C++ language; formal specification; object-oriented programming; refinement calculus; C++; COOZ; OO formal specification; data refinement; development models; formal software development approach; frame transition rule; object oriented construct; object oriented frame; operation refinement; refinement calculus; Application software; Calculus; Formal specifications; Laboratories; Large-scale systems; Object oriented modeling; Programming;

fLanguage

English

Publisher

ieee

Conference_Titel

Technology of Object-Oriented Languages and Systems, 1999. TOOLS 31. Proceedings

Conference_Location

Nanjing

Print_ISBN

0-7695-0393-4

Type

conf

DOI

10.1109/TOOLS.1999.796492

Filename

796492