Rewriting Logic Semantics of Java

From FSL
Jump to: navigation, search

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. Online-sm.JPG

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


  • JavaRL: the rewrite logic based Java interpreter. Online-sm.JPG
  1) Download the Maude-based rewriting specification of Java above
  2) Download the JavaRL package
  3) Uncompress the downloaded packages
  4) Modify the 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)
  Java -cp <javarl-dir> javarl.JavaRL -cls class-path [Options] [MainClass]
  -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 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

Related Publications

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
Formal Analysis of Java Programs in JavaFAN 
Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
CAV'04, LNCS 3114, pp 501 - 505. 2004.

Personal tools