Title :
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
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;
Conference_Titel :
Technology of Object-Oriented Languages and Systems, 1999. TOOLS 31. Proceedings
Conference_Location :
Nanjing
Print_ISBN :
0-7695-0393-4
DOI :
10.1109/TOOLS.1999.796492
