通过翻译为 ML 对 MiniJava 程序进行分析

MiniJava 是面向对象编程语言 Java 的一个子集。Standard ML 是 ML 函数式编程语言家族的典型代表，该家族包括 F# 和 OCaml。针对类 Java 和类 ML 的语言，已开发出不同的程序分析与验证工具及技术。自然地，为特定语言开发的工具强调对该语言中常用语言特性的精确处理。在 Java 中，这意味着具有可变属性的对象和动态方法分派。在 ML 中，这意味着高阶函数和带模式匹配的代数数据类型。我们提议将程序从一种语言翻译为另一种语言，并利用目标语言的工具进行分析与验证。通过这样做，我们希望识别目标语言工具中需要改进的地方，并建议可能源自源语言工具的技术以指导其改进。更一般地，我们希望开发对代码风格和数据表示变化更具韧性的程序推理工具。我们通过概述一个仅使用 ML 核心特性（特别地，避免使用 ML 的可变引用）的从 MiniJava 到 ML 的翻译来启动我们的计划。