The Operational Semantics For RCOS And Its Application In Program Analysis

rCOS is short for A Refinement Calculus for Object Systems, which is known as a refinement calculus for object oriented systems. rCOS presents a mathematical characterization of object-oriented concepts and is based on the predicate logic in Hoare and He's Unifying Theories of Programming(UTP). It is similar to Java and C++ and captures the feature of subtypes, visibility, reference types, inheritance and so on.In the paper, we first present a kind of structure operational semantics for rCOS.The given operational semantics play a great important in programming analyse, especially in the design pat-tern recognition [8,9].To construct the abstract model from rCOS instead of analyzing directly on source code, we combine static and dynamic analysis together to achieve better checking effi-ciency. Class diagrams and object graphs are obtained with the analysis of rCOS program. The given operational semantics for rCOS with the object graph is given as the basis for representing object relationships.A relational calculus is proposed to specify the pattern properties we would like to check. We classify two categories of property for patterns:general property and user-related property. A gen-eral algorithm for calculating relational predicates is presented to perform the property checking. The examples of design patterns from GoF [5], such as abstract factory pattern, observer pattern, composite pattern etc, are also provided to illustrate the effectiveness of our approach from which we can tell whether some patterns are used correctly. Finally we implement a tool and do some ex-periment to check design pattern through static and dynamic ways. Thus we finish the goal that to check whether design patterns are used correctly in order to achieve the goals that design patterns can be identified automatically (good pattern are found or bad pattern may exist in systems).