Formalisation of a frame stack semantics for a Java-like language

TL;DR

This paper formalizes a Java-like language's operational semantics using Coq, enabling proofs of invariants and properties related to method execution, and introduces a type system for classifying compound values and functions.

Contribution

It presents a novel Coq formalisation of small-step semantics for a Java-like language with explicit frame stack manipulation, and develops a type system for compound values and extensional methods.

Findings

Mechanised proof of semantics consistency between typed and untyped versions

Formalisation allows specifying and proving invariants at each computation step

Experiments support the formalisation approach

Abstract

We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a compound value and classify certain methods as extensional functions operating on them. In our formalisation we make a mechanised proof that the operational semantics for the untyped version of the semantics agrees with the one for the typed one. We discuss different methods to make such formalisation effort and provide experiments that substantiate it.