CSM-471: Abstract Semantics for Java 1.4 Programs

This document is a compendium of examples that describe the entities and relations that represent the abstract semantics (finite structures) of programs in the JavaTM programming language. It is designed to provide further explanation to the definitions given in the LePUS3 and Class-Z Reference manual [Eden et al. 2007]. To remind the reader, a finite structure is a simplified ('abstracted') picture of the program, which 'flattens' the knotty structure and syntax of the source code into a set of primitive entities (also called entities of dimension 0) and relations. Essentially, each finite structure can be viewed as a relational database, or a set of tables which contain tuples of entities ('records'). Below we list a few sample Java programs and the finite structure that represents them.