Rewriting Logic Semantics of Java
The current rewriting specification of Java semantics is based on the Java Language Specification, Second Edition. Written in Maude, this semantic specification is executable and can be used to formally analyze Java programs without extra effort. A Java interpreter, named JavaRL, is implemented based on this rewriting logic based semantic specification, which hides details of the underlying rewrite logic and automates the formal analysis of Java programs.
Related projects: Rewriting Logic Semantics, JavaFAN
News and Changes
- 2006-11-14: JavaRL 1.0, the rewrite logic based Java interpreter, has been released
- 2006-11-10: The Maude-based rewriting semantic specification of Java (version 0.3) has been released
- Maude-based rewriting specification of Java (Ver 0.3) (It is still under testing and evolving.)
- JavaRL: the rewrite logic based Java interpreter.
Installation: 1) Download the Maude-based rewriting specification of Java above 2) Download the JavaRL package 3) Uncompress the downloaded packages 4) Modify the JavaRLConfiguration.properties file in the javarl directory as follows: - MaudePath: the path to the Maude executable - SpecPath: the path to the directory containing the Java semantic specifications (not the JavaRL executables!) - MCPath: the path to the Maude model checker file (model-checker.maude)
Usage: Java -cp <javarl-dir> javarl.JavaRL -cls class-path [Options] [MainClass] Options: -cls class-path : the path contains all the Java files involved in the program MainClass : the entry class of the program; if ignored, the first class in the class path with the main method will be used -maudecode : output the Maude module translated from the original program -mc property-file: model check the specified property -s deadlock: search for deadlock -reformat : output the preprocessed Java file only -op output-path : store the output to the designated file; otherwise, the output will be printed to the standard output
For example, assuming that both javarl and java-rl-spec were unzipped in the current directory, and that a HelloWorld.java example (containing a HelloWorld class with a main method) is in the example directory. Then one can run the HelloWorld program by using the command:
java -cp . javarl.JavaRL -cls examples HelloWorld
- A Rewriting Logic Approach to Static Checking of Units of Measurement in C
- Mark Hills, Feng Chen and Grigore Rosu
RULE'08, ENTCS, to appear, 2008
PDF, RULE'08 slides, RULE'08, BIB
- 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
PDF, TR@UIUC, BIB
- Formal Analysis of Java Programs in JavaFAN
- Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
CAV'04, LNCS 3114, pp 501 - 505. 2004.
PDF, LNCS, CAV'04, DBLP, BIB