Proof Transformation via Interpretation Functions: Results, Problems and Applications
journal contributionposted 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.
CitationElectronic Notes in Theoretical Computer Science, 2005
Author affiliation/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science
SourceProceedings 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
- VoR (Version of Record)