From FSL
Jump to: navigation, search



The KOOL language is a dynamic object-oriented language, somewhat in the spirit of Smalltalk (at least in terms of the language, since we do not have Smalltalk-like object browers, etc, but we do have a class-based, not object-based or prototype, language), that we are using in FSL for our research in programming languages, language semantics, and rewriting logic. KOOL stands for K-based Object Oriented Language. It is defined using the K framework and implemented in the rewriting logic engine Maude. Although we think that KOOL is an interesting langauge, it is not offered as an example necessarily of how to define OO languages, but instead gives us a good platform for research. We currently have not introduced any new features into the language (meaning no language features are especially novel), although we do plan to in the future.

Current Release

Our current release is version 1.3. Files in this distribution include the basic files, some samples, and a parser, written using SDF and C, that takes a KOOL language program and translates it into a Maude format. To run the examples, you will need Maude. The examples have been tested using Maude 2.3. Note: you will need to build the program that translates from ATerms to Maude, named koolcc. To do so, in the kool-parser directory run program buildcc.sh.

Alternative Releases

We have spend some time working on various alternatives. There are included below. These may not be kept up to date with the main KOOL distribution.


UPDATED 6 February 2008: The 1.3 release of KOOL includes garbage collection, and also provides an option (based on changed in the Maude semantics at this point) to either enable or disable boxing. The memory model has been changed quite a bit, so instead of having separate memory pools a flag on the location indicates whether it is shared or not. Examples from the recent WRLA submission are included for performance testing purposes. Note that we are also adding vectors; the GC does not yet work with vectors, but should soon.

UPDATED 19 February 2007:The version of KOOL with synchronized methods has been posted under Alternative Releases, above. This also uses the new runkool command, although any examples using runkool.sh will still work if runkool.sh is used. Running runkool with the --help flag gives additional details, including translations from old to new commands.

UPDATED 16 February 2007:The update to version 1.2 includes a new method for running KOOL programs, the runkool command. This consolidates several run commands that have been introduced to handle different run cases, like running the model checker or running with a custom .maude file (to add new model checking propositions, for instance). This also includes better usage details and more flexible commands. The original files, runkool.sh, mckool.sh, and mccust.sh, are still included, so any commands shown in papers will still work, but should be considered deprecated. Also included are changes shown in recent papers, such as the use of memory pools and scalar values with auto-boxing. Versions without these features will be posted soon in case anyone wants to compare performance between different feature sets.

UPDATED 15 November 2006:Someone pointed out that the parser did not include the C source code that translates the SDF output into Maude. That is now included as koolcc.c above.

UPDATED 18 October 2006:The update to version 1.1 makes some fairly significant structural changes. The most noticeable is that primitives are now available for invocation directly in language files. This means that the prelude classes (such as Integer) can now be written directly in KOOL, instead of needing to be coded into their processed, continuation-based forms. A new type of class declaration, primclass, is used to represent classes which can hold primitive values. This seems safer than using designated variable names to hold the primitive value. The prelude classes are now defined in prelude.kool, which is now included above. Additional changes to the prelude should be coming soon. Also, it is important to note that the changes have not yet been backported to the non-concurrent version of KOOL -- they are only in Concurrent KOOL. Since Concurrent KOOL can run any programs that standard KOOL can, it's best for now to just use Concurrent KOOL.

UPDATED 17 April 2006:The update to version 1.01 adds two exceptions defined in the semantics which were missing from the definition, the NilPointerException and the MethodNotFoundException. The first is triggered when an invocation is attempted from a Nil pointer. The second is triggered when an appropriate message is not found on the target object. The input capabilities have also been extended, so now it is possible to read in values of type String, Integer, Float, and Boolean. The input is still not easy to use, since the ATerm -> Maude compiler doesn't know about input yet. We are currently working on this, so input should be easier to use soon. Conversions are now available from String objects to Integer, Float, and Boolean objects, with appropriate names (toInteger, toFloat, and toBoolean). An example of these operations is contained in sample file IO1.kool. Finally, nil is now available as an expression, so it is possible to assign nil to object references. An example is Assign1.kool.

You don't need the parser unless you plan to write your own programs -- the samples include programs in both KOOL and Maude format. If you wish to write your own programs, you will need to download Stratego/XT, SDF, and the ATerm library. These are all available at the Stratego download page. Specifically, we have tested with version 2.4.2 of the ATerm library, version 2.3.3 of SDF, and version 0.16 of Stratego. You will also need a C compiler. We use gcc, but any standard C compiler should work. We have only tested on Linux.

To build the parser, in the kool-parser directory you will first need to run pack.sh, which will create a .def file from all the .sdf files. This step only needs to be run if you have changed any of the .sdf files, otherwise you can use the provided .def file. You may need to modify this file, based on the install location you choose for SDF, since it pulls some standard SDF-provided definitions for whitespace. Then, run gentable.sh to generate a parse table. Again, this only needs to be done if the .def file has changed, otherwise the existing parse table can be used. These two steps are combined in refresh.sh. To compile the C file that converts from ATerm format to Maude, just run buildcc.sh, which will generate a file named koolcc. Now, to actually compile a file, you can use the provided build.sh script as an example. This script assumes that koolcc is linked or copied to the parent of the kool-parser directory. Finally, to run the program, start maude with the maude command, then load either kool.maude or c-kool.maude (you must use the latter if you spawn threads or acquire/release locks, but otherwise they are identical), and finally use the in command (like in mysample.maude) to load the file. This entire process is automated in the sample runkool.sh script. Note we still need to automate a couple of generation steps, including allowing input to easily be added to the .maude file that is used for the execution and allowing a different eval to be used (concurrency has two, eval and eval*, the first of which exits when the main thread finishes, with the second waiting for all threads to finish).

Hopefully we will have a working KOOL interpreter on our site soon that will allow a KOOL program to be written in a text field on an HTML form and then submitted, returning parsing errors or program output.

Please contact us with any questions.


There are several related publications on KOOL. A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages is the first which includes KOOL, and also includes material on the definition of Java. KOOL: A K-based Object-Oriented Language is the manual for KOOL, and is meant to stay in sync with the language as it evolves. It includes the most information about KOOL, but the least context, with a lesser focus on related work and comparisons to other languages and definitional frameworks. A Rewriting Based Approach to OO Language Prototyping and Design contains less information on KOOL than the KOOL manual, but is more up to date than A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages, and contains additional contextual material, comparing the K technique to other styles of semantics and providing references to other languages and definitional environments. On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance focuses on how the design of the rewriting-logic semantics of KOOL can impact the performance of analysis; variant design are presented with performance measures. Finally, KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis describes the KOOL language and system in a concise (10-page) format, providing an overview of the current runtime support for KOOL as well as discussion of a synchronized methods addition to the language.

KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis 
Mark Hills and Grigore Rosu
RTA'07, LNCS 4533, pp 246-256. 2007
PDF, RTA'07 slides, LNCS, RTA'07, BIB

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

A Rewriting Based Approach to OO Language Prototyping and Design 
Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2786, October 2006

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

Personal tools