Abstract

Java is currently a widely used programming language. However, there is no formal definition of Java's semantics. Consequently, Java code does not have a universal meaning. This work discusses recent attempts to formalize Java and presents a new formalism of Java called Javalite. In contrast to common approaches to formalization, Javalite is purely syntactic in its definition. Syntactic operational semantics use the structure of the language to define its behavior. Javalite models most Java features with notable exceptions being threads, reflection, and interfaces. This work presents an executable semi-formal model of Javalite in PLT Redex. Being executable means that Javalite programs can be run using this model. We then render the semi-formal model in the Coq theorem prover and present theorems stating that the operational semantics are decidable and deterministic. This formal model can then be used to facilitate research in areas such as proving properties of algorithms that perform various analyses on Java code, e.g. verification, optimization, and refactoring.

Degree

College and Department

Physical and Mathematical Sciences; Computer Science

Rights

http://lib.byu.edu/about/copyright/