A rigorous approach for proving model refactorings

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A rigorous approach for proving model refactorings

Full text

Pdf (120 KB)

Source

Automated Software Engineering archive
Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering table of contents

Long Beach, CA, USA

SESSION: Short papers 2 table of contents

Pages: 372 - 375

Year of Publication: 2005

ISBN:1-59593-993-4

Authors

Rohit Gheyi	Federal University of Pernambuco, Recife, Brazil
Tiago Massoni	Federal University of Pernambuco, Recife, Brazil
Paulo Borba	Federal University of Pernambuco, Recife, Brazil

Sponsors

ACM: Association for Computing Machinery
SIGART: ACM Special Interest Group on Artificial Intelligence
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 29, Citation Count: 2

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1101908.1101973 What is a DOI?

ABSTRACT

Both model and program refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics. In this paper, we propose guidelines on how to rigorously prove model refactorings for Alloy, a formal object-oriented modeling language. We use the Prototype Verification System (PVS) to specify and prove the soundness of the transformations. Proposing refactorings in this way can facilitate not only design, but also improve the quality of refactoring tools.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
	2	Jonathan Edwards , Daniel Jackson , Emina Torlak, A type system for object models, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
	3	Refactoring: improving the design of existing code, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	4	R. Gheyi, T. Massoni, and P. Borba. Basic Laws of Object Modeling. In 3rd Specification and Verification of Component-Based Systems, pages 18--25, 2004.
	5	R. Gheyi, T. Massoni, and P. Borba. An Abstract Equivalence Notion for Object Models. Electronic Notes in Theoretical Computer Science, 130:3--21, 2005.
	6	Daniel Jackson , Ilya Shlyakhter , Manu Sridharan, A micromodularity mechanism, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
	7	S. Owre et al. PVS System Home Page. At http://pvs.csl.sri.com.

CITED BY 2

	Rohit Gheyi , Tiago Massoni, Formal refactorings for object models, Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	Rohit Gheyi , Tiago Massoni , Paulo Borba, A Static Semantics for Alloy and its Impact in Refactorings, Electronic Notes in Theoretical Computer Science (ENTCS), 184, p.209-233, July, 2007