Paper Info
Title
A Formal Software Development Approach Based on COOZ and Refinement Calculus
Abstract
The advantage of COOZ is to specify a large scale software, but not support refinement calculus and need to proof in refinement. Thus its application is confined and it can not be taken as the whole method for software development. Including Refinement Calculus into COOZ complements its disadvantage during design and implement. The apartment between design and implement for construct and notation is removed as well. Then the software can be developed smoothly in the same frame. There is not corespondent object-oriented construct in existing Refinement Calculus. The combine of COOZ and Refinement Calculus can built a object-oriented frame, in which the specification in COOZ is refined stepwise to code by calculus. In the paper ,two development model is argued ,which are based mainly on COOZ and Refinement Calculus respectively. The first model is debated primarily. The data refinement and operation refinement is analyzed by example; the two method of operation refinement for OO formal specification is discussed simply; the frame transition rule from COOZ to C++ is argued. For second model ,a class model and the class data refinement calculus is argued, which can be as a base of OO extension for Refinement Calculus.
Year
DOI
Venue
1999
10.1109/TOOLS.1999.796492
TOOLS
Keywords
DocType
ISBN
refinement calculus,application software,c,formal specifications,programming,formal specification,object oriented programming,calculus
Conference
0-7695-0393-4
Citations 
PageRank 
References 
0
0.34
9
Authors
5
Name
Order
Citations
PageRank
Yunfeng Wang130931.38
Bixin Li243951.11
Jun Pang352130.59
Ming Zha401.01
guoliang zheng56515.24