Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation - Supplemental Material

This is the appendix to the iFM 2023 paper "Joining Forces! Reusing Contracts for Deductive Verifiers through Automatic Translation". Due to publisher constraints, it had to be moved online after the paper was peer-reviewed. The appendix contains the grammar for the intermediate representation used by the tool that the paper describes.<br>Paper abstract:Deductive verifiers can be used to prove the correctness of programs by specifying the program's intended behaviour using annotations such as pre- and postconditions. Unfortunately, most verifiers use their own unique specification language for those contract-based annotations. While many of them have similar concepts and syntax, there are numerous semantic differences and subtleties that make it very difficult to reuse specifications between verifiers. But reusing specifications could help overcome one of the bottlenecks of deductive verification, namely writing specifications. Therefore, we present the Specification Translator, a tool to automatically translate annotations for deductive verifiers. It currently supports Java programs annotated for OpenJML, Krakatoa and VerCors. Using the Specification Translator, we show that we can reuse 81% of the annotations, which would otherwise need to be manually translated. Moreover, it allows to reuse tools such as Daikon that generate annotations only in the syntax of one specific tool.本文件为iFM 2023会议论文《携手赋能！基于自动翻译的演绎验证器契约复用》的附录。由于出版社限制，该附录在论文完成同行评议后仅能线上发布。本附录包含该论文所介绍工具所使用的中间表示（intermediate representation）的语法规范。<br>论文摘要：演绎验证器（Deductive verifiers）可通过前置条件（preconditions）、后置条件（postconditions）等注解形式指定程序的预期行为，以此证明程序的正确性。但遗憾的是，绝大多数验证器都拥有各自专属的契约式注解（contract-based annotations）规范语言。尽管这类语言在概念与语法上多有相似之处，但语义层面的诸多差异与细微区别，使得不同验证器之间的注解复用难度极高。不过注解复用能够帮助突破演绎验证的核心瓶颈之一——注解编写工作。为此，本文提出了规范翻译器（Specification Translator），一款可自动转换演绎验证器所需注解的工具。目前该工具支持针对OpenJML、Krakatoa与VerCors三类工具注解的Java程序。通过规范翻译器，我们可复用81%的原有注解，而这些注解原本需要通过手动方式完成转换。此外，该工具还支持复用如Daikon这类仅能生成单一工具语法格式注解的生成工具。