%0 Journal Article %1 kosiuczenko_05_proof %A Kosiuczenko, Piotr %B Proceedings of the Workshop on Software Evolution through Transformations: Model-based vs. Implementation-level Solutions (SETra 2004) %D 2005 %J Electronic Notes in Theoretical Computer Science %K 2005 statecharts proof uml transformation %N 3 %P 139--145 %R 10.1016/j.entcs.2004.08.040 %T Proof Transformation via Interpretation Functions: Results, Problems and Applications %U http://dx.doi.org/10.1016/j.entcs.2004.08.040 %V 127 %X 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.

@article{kosiuczenko_05_proof, 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.}, added-at = {2009-02-11T21:03:05.000+0100}, author = {Kosiuczenko, Piotr}, biburl = {https://www.bibsonomy.org/bibtex/2ae0dcb94e5482a02ed94367dc88294d6/leonardo}, booktitle = {Proceedings of the Workshop on Software Evolution through Transformations: Model-based vs. Implementation-level Solutions (SETra 2004)}, citeulike-article-id = {2941829}, doi = {10.1016/j.entcs.2004.08.040}, interhash = {410e6a1f5ac59004c94b3a3dff49a59b}, intrahash = {ae0dcb94e5482a02ed94367dc88294d6}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {2005 statecharts proof uml transformation}, month = {April}, number = 3, pages = {139--145}, posted-at = {2008-06-29 17:09:24}, priority = {2}, timestamp = {2009-02-11T21:03:05.000+0100}, title = {Proof Transformation via Interpretation Functions: Results, Problems and Applications}, url = {http://dx.doi.org/10.1016/j.entcs.2004.08.040}, volume = 127, year = 2005 }