A rewriting approach to the design and evolution of object-oriented languages

ABSTRACT

Rewriting logic semantics provides an environment for defining new and existing languages. These language definitions are formal and executable, providing language interpreters almost for free while also providing a framework for building analysis tools, such as type checkers, model checkers, and abstract interpreters. Large subsets of several existing object-oriented languages have been defined, while a new research language, KOOL, has been created as a platform for experimenting with language features and type systems. At the same time, new tools and formalisms aimed specifically at programming languages are being developed.

REFERENCES

• 1: G. Bracha. Pluggable type systems. Revival of Dynamic Languages workshop at OOPSLA 2004, October 2004.
• 2: F. Chen, M. Hills, and G. Rosu. A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages. Technical Report UIUCDCS-R-2006-2702, University of Illinois at Urbana-Champaign, 2006.
• 3: M. Clavel , F. Durán , S. Eker , P. Lincoln , N. Martí-Oliet , J. Meseguer , J. F. Quesada, Maude: specification and programming in rewriting logic, Theoretical Computer Science, v.285 n.2, p.187-243, 28 August 2002 [doi>10.1016/S0304-3975(01)00359-0]
• 4: A. Farzan, F. Chen, J. Meseguer, and G. Rosu. Formal Analysis of Java Programs in JavaFAN. In Proceedings of CAV'04, volume 3114 of LNCS, pages 501--505. Springer, 2004.
• 5: Adele Goldberg , David Robson, Smalltalk-80: the language and its implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• 6: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 7: M. Hills, T. B. Aktemur, and G. Rosu. An Executable Semantic Definition of the Beta Language using Rewriting Logic. Technical Report UIUCDCS-R-2005-2650, University of Illinois at Urbana-Champaign, 2005.
• 8: Mark Hills , Traian Şerbănuţă , Grigore Roşu, A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters, Electronic Notes in Theoretical Computer Science (ENTCS), v.176 n.4, p.215-231, July, 2007 [doi>10.1016/j.entcs.2007.06.017]
• 9: M. Hills and G. Rosu. KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis. In Proceedings of RTA'07, volume 4533 of LNCS, pages 246--256. Springer, 2007.
• 10: M. Hills and G. Rosu. On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance. In Proceedings of FMOODS'07, volume 4468 of LNCS, pages 107--121. Springer, 2007.
• 11: Ole Lehrmann Madsen , Birger Mø-Pedersen , Kristen Nygaard, Object-oriented programming in the BETA programming language, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1993
• 12: José Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, v.96 n.1, p.73-155, 6 April 1992
• 13: José Meseguer , Grigore Rou, The rewriting logic semantics project, Theoretical Computer Science, v.373 n.3, p.213-237, April, 2007 [doi>10.1016/j.tcs.2006.12.018]
• 14: Peter D. Mosses, The Varieties of Programming Language Semantics, Revised Papers from the 4th International Andrei Ershov Memorial Conference on Perspectives of System Informatics: Akademgorodok, Novosibirsk, Russia, p.165-190, July 02-06, 2001
• 15: G. Rosu. K: a Rewrite Logic Framework for Language Design, Semantics, Analysis and Implementation. Technical Report UIUCDCS-R-2006-2802, University of Illinois at Urbana-Champaign, 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Design, Languages

Keywords:
formal analysis, language design, language semantics, object-oriented languages, rewriting logic