Introducing reference semantics via refinement

Two types of semantics have been given to object-oriented formal specification languages. Value semantics denote a class by a set of values representing its objects. Reference semantics denote a class by a set of references, or pointers, to values representing its objects. While adopting the former facilitates formal reasoning, adopting the latter facilitates transformation to object-oriented code. In this paper, we propose a combined approach using value semantics for abstract specification and reasoning, and then refining to a reference semantics before transforming specification to code.

Towards pattern-based design recovery

A method and a corresponding tool is described which assist design recovery and program understanding by recognising instances of design patterns semi-automatically. The approach taken is specifically designed to overcome the existing scalability problems caused by many design and implementation variants of design pattern instances. Our approach is based on a new recognition algorithm which works incrementally rather than trying to analyse a possibly large software system in one pass without any human intervention. The new algorithm exploits domain and context knowledge given by a reverse engineer and by a special underlying data structure, namely a special form of an annotated abstract syntax graph. A comparative and quantitative evaluation of applying the approach to the Java AWT and JGL libraries is also given.

A formal metamodeling approach to a transformation between the UML state machine and object-z

A significant problem with currently suggested approaches for transforming between models in different languages is that the transformation is often described imprecisely, with the result that the overall transformation task may be imprecise, incomplete and inconsistent. This paper presents a formal metamodeling approach for transforming between UML and Object-Z. In the paper, the two languages are defined in terms of their formal metamodels, and a systematic transformation between the models is provided at the meta-level in terms of formal mapping functions. As a consequence, we can provide a precise, consistent and complete transformation between them.