On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance
From FSL
This paper is part of our ongoing work on Rewriting Logic Semantics, investigating the impact of language design decisions in the object-oriented language KOOL on the performance of analysis techniques, such as breadth-first state space search and model checking. The technical report version includes some additional information about the modifications to KOOL, including a listing of changes to the parser and the language semantics.
[edit] On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance
- Mark Hills and Grigore Rosu
- FMOODS'07, LNCS 4468, pp 107-121, 2007
- Abstract. Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. This flexibility in design can lead to problems during analysis, as different designs for the same language feature can cause drastic differences in analysis performance. This paper describes some of these design decisions in the context of KOOL, a concurrent, dynamic, object-oriented language. Also described is a general mechanism used in KOOL to support model checking while still allowing for ongoing, sometimes major, changes to the language definition.
[edit] Technical Report Version
- Mark Hills and Grigore Rosu
- Technical report UIUCDCS-R-2007-2809, January 2007
- Abstract. Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. This flexibility in design can lead to problems during analysis, as different designs for the same language feature can cause drastic differences in analysis performance. This paper describes some of these design decisions in the context of KOOL, a concurrent, dynamic, object-oriented language. Also described is a general mechanism used in KOOL to support model checking while still allowing for ongoing, sometimes major, changes to the language definition.
