JAS (Java Action Semantics)

As a pilot study, I have written an action-semantic specification of the abstract syntax and dynamic semantics of JOOS (available in Postscript). JOOS is a Java subset designed by Laurie Hendren. It demonstrates the main concepts of Java: classes, inheritance, dynamic method selection, constructors. JOOS lacks static fields and methods, and automatic type conversions. All fields are private, and fields may not be hidden. All methods and constructors are public, and they may not be overloaded.