Using CafeOBJ to mechanise refactoring proofs and application. (English) Zbl 1279.68113

Sampaio, Augusto (ed.), Proceedings of the second Brazilian symposium on formal methods (SBMF 2005), Porto Alegre, RS, Brazil, November 30, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 184, 39-61 (2007).
Summary: We show how rewriting systems, in particular CafeOBJ, can be used to automatically prove refactoring rules. In addition, a small case study that illustrates the application of a refactoring rule in an arbitrary program is also developed. Our approach is based on a sequential object-oriented language of refinement (rool) similar to Java. We have implemented the rool grammar in CafeOBJ, as well as the laws that define its semantics. Each refactoring rule is derived by the application of these laws, in a constructive way. The refactorings are also implemented in CafeOBJ, allowing the reduction of an arbitrary program.
For the entire collection see [Zbl 1275.68031].


68Q42 Grammars and rewriting systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)


Eiffel; OBJ3; Maude
Full Text: DOI


[1] Arnold, K.; Gosling, J., The Java programming language, (1996), Addison-Wesley · Zbl 0876.68015
[2] Back, R.J.R., Procedural Abstraction in the Refinement Calculus, Technical report, Department of Computer Science, Abo - Finland (1987)
[3] Cavalcanti, A.L.C.; Naumann, D., A weakest precondition semantics for refinement of object-oriented programs, IEEE transactions on software engineering, 26, 713-728, (2000)
[4] Cavalcanti, A.L.C.; Naumann, D.A., A weakest precondition semantics for an object-oriented language of refinement, (), 1439-1459 · Zbl 0953.68081
[5] Cavalcanti, A.L.C.; Sampaio, A.; Woodcock, J.C.P., An inconsistency in procedures, parameters and substitution in the refinement calculus, Science of computer programming, 33, 87-96, (1999) · Zbl 0942.68014
[6] Cinnéide, M.Ó. and P. Nixon, Automated application of design patterns to legacy code., in: ECOOP Workshops, 1999, p. 176
[7] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., Maude manual (version 2.1), (2004), SRI International
[8] Cornélio, M., “Refactoring as Formal Refinements,” Ph.D. thesis, Universidade Federal de Pernambuco (2004)
[9] Dijkstra, E.W., A discipline of programming, (1976), Prentice Hall · Zbl 0368.68005
[10] Fowler, M., Refactoring: improving the design of existing code, Addison-wesley object technology series, (1999), Addison-Wesley · Zbl 1020.68632
[11] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J., Introducing OBJ, (), Cambridge
[12] Lano, K., J. Bicarregui and S. Goldsack, Formalising design patterns, in: D. Duke and A. Evans, editors, 1st BCS-FACS Northern Formal Methods Workshop, Ilkley, UK, Electronic Workshops in Computing, 1996. URL http://www.ewic.org.uk/ewic/workshop/view.cfm/NFM-96
[13] Larman, C., Applying UML and patterns, (2002), Prentice Hall
[14] Lira, B.O., A.L.C. Cavalcanti and A.C.A. Sampaio, Automation of a Normal Form Reduction Strategy for Object-oriented Programming, in: Proceedings of the 5th Brazilian Workshop on Formal Methods, 2002, pp. 193-208
[15] Meyer, B., Object-oriented software construction, (1997), Prentice Hall · Zbl 0987.68516
[16] Morgan, C.C., Programming from specifications, (1994), Prentice Hall · Zbl 0829.68083
[17] Morgan, C.C., K.A. Robinson and P.H.B. Gardiner, On the Refinement Calculus, Technical Monograph PRG-70, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (1988)
[18] Nakagawa, A.; Sawada, T.; Futatsugi, K., Cafeobj User’s manual - ver. 1.4.2, 1999, (1999), Disponível em
[19] Opdyke, W.F., “Refactoring Object-Oriented Frameworks,” Ph.D. thesis, Urbana-Champaign, IL, USA (1992). URL citeseer.ist.psu.edu/article/opdyke92refactoring.html
[20] Silva, A.L.; Menezes, M.M.; Silva, L., Using cafeobj to implement a reduction strategy in the context of hardware/software partitioning, Electronic notes in theoretical computer science, 95, 63-82, (2004)
[21] Tokuda, L., “Evolving Object-Oriented Designs With Refactorings,” Ph.D. thesis, University of Texas at Austin (1999) · Zbl 0963.68558
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.