Programming Languages: Semantics and Implementation

In the research reported here, the ASM (Abstract State Machines) method has been used to develop a method for defining and analysing, in a rigorous but concise, complete but programmer friendly way, the dynamic semantics of real-life programming languages and of their implementation on virtual or real machines. The covered programming paradigms include

The operational and abstract character of ASMs

For a systematic exposition of the ASM systems engineering method in its full generality see the AsmBook. For machine supported programming language design the method provides a framework which permits the mathematical analysis (verification and validation) of both program behaviour and of language implementations. In particular proven to be correct and machine checked language compilation schemes have been obtained from Java to JVM code, from Occam to Transputer code, from Prolog to WAM code in the references given above.

A survey for 1989-2013is available from Journal of Logic and Computation (2014) elaborated from an invited lecture at the MS Research Workshop on Scalabe Language Specification (Cambridge 2013).

Book

Java and the JavaVirtual Machine: Definition, Verification, Validation

(by R. Stärk, J. Schmid, E. Börger, Springer-Verlag, 2001)

This book provides a structured and high-level description, together with a mathematical and an experimental analysis, of Java and of the Java Virtual Machine (JVM), including the standard compilation of Java programs to JVM code and the security critical bytecode verifier component of the JVM. The following fundamental property of JVM verification and execution of compiled Java programs is analysed and proved:

Under explicitly stated conditions, any well-formed and well-typed Java program, when correctly compiled, passes the verifier and is executed on the JVM. It executes without violating any run-time checks, and is correct with respect to the expected behavior as defined by the Java machine.

The description is structured into modules, and its abstract character implies that it is truly platform and programming language independent. It comes with a natural refinement to executable machines on which code can be tested. The method we develop for this purpose can be applied to other virtual machines and to other programming languages as well.

The method developed in this book has been reused in 2003 to model and analyse the static and dynamic semantics of C# ( Draft, Final version in TCS 336, 2005), including an analysis of the .NET exception handling mechanism ( Draft, Final version in JOT 3.5 (2006) 5-34)

Papers