2005

Redesign of UML Class Diagrams: A Formal Approach

CS-05-001 P. Kosiuczenko.

Contracts provide a precise way of specifying object-oriented systems. When a class structure is modified, the corresponding contracts must be modified accordingly. This paper presents a method of transforming contracts, which allows the extension of a mapping defined on a few model elements, to - what we call - an interpretation function, and to use this function to automatically translate OCL-constraints. Interestingly, such functions preserve reasoning using prepositional calculi, resolution, equations, and induction. Interpretation functions can be used to trace model elements throughout multiple redesigns of UML class diagrams in both the forward, and the backward direction. The applicability of our approach is demonstrated in several examples, including some of Fowler's refactoring patterns.

Keywords: UML, OCL, formal methods, refactoring, requirements tracing.

Available as: Adobe™ PDF (.pdf)

Proof Transformation via Interpretation Functions

CS-05-002 P. Kosiuczenko.

Redesign of a class structure requires transformation of the corresponding specification. In a previous paper we have shown how to use, what we call, interpretation functions for transformation of constraints. In this paper we study the way proof are transformed via such functions. We provide a sufficient condition for interpretation functions to preserve proofs using propositional logic with modus ponens, proofs using resolution rule and induction.

Available as: Adobe™ PDF (.pdf)

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc  seadmissions@le.ac.uk
E: MSc  pgadmissions@le.ac.uk

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604
E: csadmin@mcs.le.ac.uk

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom

Accessibility

DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.