University of Leicester
Browse

Proof Transformation via Interpretation Functions: Results, Problems and Applications

Download (201.07 kB)
journal contribution
posted on 2016-10-31, 15:15 authored by Piotr Kosiuczenko
Change is a constant factor in Software Engineering process. Redesign of a class structure requires transformation of the corresponding OCL constraints. In a previous paper we have shown how to use, what we call, interpretation functions for transformation of constraints. In this paper we discuss recently obtained results concerning proof transformations via such functions. In particular we detail the fact that they preserve proofs in equational logic, as well as proofs in other logical systems like propositional logic with modus ponens or proofs using resolution rule. Those results have direct applications to redesign of UML State Machines and Sequence Diagrams. If states in a State Machine are interpreted by State Invariants, then the topological relations between its states can be interpreted as logical relations between the corresponding formulas. Preservation of the consequence relation can bee seen as preservation of the topology of State Machines. We indicate also an unsolved problem and discuss the mining of its positive solution.

History

Citation

Electronic Notes in Theoretical Computer Science, 2005

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Source

Proceedings of the Workshop on Software Evolution through Transformations: Model-based vs. Implementation-level Solutions (SETra 2004), Software Evolution through Transformations: Model-based vs. lmplementation-level Solutions 2004

Version

  • VoR (Version of Record)

Published in

Electronic Notes in Theoretical Computer Science

Publisher

Elsevier

issn

1571-0661

eissn

1571-0661

Available date

2016-10-31

Publisher version

http://www.sciencedirect.com/science/article/pii/S1571066105001453

Temporal coverage: start date

2004-10-02

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC