A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages

From FSL
Jump to: navigation, search

This paper is part of our ongoing work on Rewriting Logic Semantics with the KOOL and Java languages. Previous work on Java can be found in Formal Analysis of Java Programs in JavaFAN . More up to date information on KOOL can be found in KOOL: A K-based Object-Oriented Language, the current reference manual for KOOL, and A Rewriting Based Approach to OO Language Prototyping and Design, which has roughly the same coverage of KOOL but provides additional context, comparing the K technique with other language definitional techniques, both within and outside of rewriting logic.

A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages

A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages
Feng Chen, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2702, March 2006
Abstract. This paper introduces a framework for rapid prototyping of object oriented programming languages and corresponding analysis tools. It is based on formal definitions of language features in rewrite logic, a simple and intuitive logic for concurrency with powerful tool support. A domain-specific front-end consisting of a notation and a technique, called K, allows for compact, modular, expressive and easy to understand and change definitions of language features. The framework is illustrated by first defining KOOL, an experimental concurrent object-oriented language with exceptions, and then by discussing the definition of JAVA. Generic rewrite logic tools, such as efficient rewrite engines and model checkers, can be used on language definitions and yield interpreters and corresponding formal program analyzers at no additional cost.
PDF, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation