基于 ACL2 在 Java 中浅嵌入的复杂 Java 代码生成器

本文描述了一个代码生成器，该生成器根据 ACL2 在 Java 中的浅嵌入，将 ACL2 构造翻译为相应的 Java 构造。从纯函数式 ACL2 代码出发，生成的 Java 代码展现出命令式与面向对象特性，如破坏性更新、循环与重载。从 ACL2 到 Java 的整体翻译相当复杂，由若干 ACL2 到 ACL2 的预翻译步骤、一个 ACL2 到 Java 的正式翻译步骤，以及若干 Java 到 Java 的后翻译步骤组成。实验表明，生成的 Java 代码比 ACL2 代码慢不了多少。该代码生成器还能识别 ACL2 对某些 Java 构造的表示，并将其翻译为 Java，这预示了一种基于 Java 在 ACL2 中浅嵌入（即反向）的代码生成方法。该代码生成器构建于一个基于 ACL2 在 Java 中深嵌入的简单 Java 代码生成器之上，并对其进行了显著扩展。