Please use this identifier to cite or link to this item:
Title: Proof Transformation via Interpretation Functions: Results, Problems and Applications
Authors: Kosiuczenko, Piotr
First Published: 5-Apr-2005
Presented at: 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
Start Date: 2-Oct-2004
Publisher: Elsevier
Citation: Electronic Notes in Theoretical Computer Science, 2005
Abstract: 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.
DOI Link: 10.1016/j.entcs.2004.08.040
ISSN: 1571-0661
eISSN: 1571-0661
Version: Publisher Version
Status: Peer-reviewed
Type: Journal Article
Rights: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported (CC BY-NC-ND 3.0)
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
1-s2.0-S1571066105001453-main.pdfPublished (publisher PDF)201.07 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.