Analysis of MiniJava programs via translation to ML

Lester, M. ORCID: https://orcid.org/0000-0002-2323-1771 (2019) Analysis of MiniJava programs via translation to ML. In: FTfJP '19: Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, 15th Jul 2019, London. doi: 10.1145/3340672.3341119

Abstract/Summary

MiniJava is a subset of the object-oriented programming language Java. Standard ML is the canonical representative of the ML family of functional programming languages, which includes F# and OCaml. Different program analysis and verification tools and techniques have been developed for both Java-like and ML-like languages. Naturally, the tools developed for a particular language emphasise accurate treatment of language features commonly used in that language. In Java, this means objects with mutable properties and dynamic method dispatch. In ML, this means higher order functions and algebraic datatypes with pattern matching. We propose to translate programs from one language into the other and use the target language's tools for analysis and verification. By doing so, we hope to identify areas for improvement in the target language's tools and suggest techniques, perhaps as used in the source language's tools, that may guide their improvement. More generally, we hope to develop tools for reasoning about programs that are more resilient to changes in the style of code and representation of data. We begin our programme by outlining a translation from MiniJava to ML that uses only the core features of ML; in particular, it avoids the use of ML's mutable references. MiniJava is a subset of the object-oriented programming language Java. Standard ML is the canonical representative of the ML family of functional programming languages, which includes F# and OCaml. Different program analysis and verification tools and techniques have been developed for both Java-like and ML-like languages. Naturally, the tools developed for a particular language emphasise accurate treatment of language features commonly used in that language. In Java, this means objects with mutable properties and dynamic method dispatch. In ML, this means higher order functions and algebraic datatypes with pattern matching. We propose to translate programs from one language into the other and use the target language's tools for analysis and verification. By doing so, we hope to identify areas for improvement in the target language's tools and suggest techniques, perhaps as used in the source language's tools, that may guide their improvement. More generally, we hope to develop tools for reasoning about programs that are more resilient to changes in the style of code and representation of data. We begin our programme by outlining a translation from MiniJava to ML that uses only the core features of ML; in particular, it avoids the use of ML's mutable references.

Item Type	Conference or Workshop Item (Paper)
URI	https://reading-clone.eprints-hosting.org/id/eprint/99157
Item Type	Conference or Workshop Item
Refereed	Yes
Divisions	Science > School of Mathematical, Physical and Computational Sciences > Department of Computer Science
Uncontrolled Keywords	Java, ML, automated verification, static analysis, program transformation
Download/View statistics	View download statistics for this item