论文标题
通过翻译为ML的Minijava计划分析
Analysis of MiniJava Programs via Translation to ML
论文作者
论文摘要
Minijava是面向对象的编程语言Java的子集。标准ML是功能编程语言的ML家族的规范代表，其中包括F＃和OCAML。已经开发了针对类似Java的语言和类似ML的语言的不同程序分析和验证工具和技术。自然，为特定语言开发的工具强调了对该语言常用的语言特征的准确处理。在Java中，这意味着具有可变属性和动态方法调度的对象。在ML中，这意味着具有模式匹配的高阶函数和代数数据类型。 我们建议将程序从一种语言转换为另一种语言，并使用目标语言的工具进行分析和验证。通过这样做，我们希望确定可以改善目标语言工具的领域，并建议使用源语言工具中使用的技术，以指导其改进。更普遍地，我们希望开发用于推理程序的工具，这些程序对代码风格和数据表示形式的变化更具弹性。我们通过概述了从Minijava到ML的翻译来开始我们的程序，该翻译仅使用ML的核心功能；特别是，它避免使用ML的可变参考。
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.
