Evaluation of Specification Inference Tools for Deductive Verification

About this artifactAs part of our research, we evaluated the impact of several specification inference tools for deductive verification.This artifact contains the following things:- input-output-examples-for-specification-inference/: A directory containing the inputs we used to test specification inference tools as well as the output that the tools ChatGPT, Daikon, EvoSpex, Strongarm and Toradocu generated.- Strongarm.ova: A Virtual Machine with the tool Strongarm installed. It also contains the examples we used to test the tool.- SpecInferenceSurveyArtifact.ova: A Virtual Machine with the tools Daikon, EvoSpex and Toradocu installed. It also contains the code, documentation and a test suite for the examples we used to test the tools. You can use the Virtual Machines to try the specification inference tools yourself.If you're only interested in the input/output we used for testing the tools, then the input-output-examples-for-specification-inference/ directory should be sufficient. License informationThe tools are shared under their original licenses which are included in the dataset.The ArrayList.java and Counter.java examples are licensed under CC-BY 4.0.The BinarySearchGood.java example is originally from https://www.openjml.org/examples and is shared under the CC-BY-NC 4.0 license.

本研究工件说明
作为本研究的一部分，我们针对若干用于演绎验证（deductive verification）的规格推断（specification inference）工具的影响开展了评估。本研究工件包含以下内容：
- input-output-examples-for-specification-inference/：该目录存放了我们用于测试规格推断工具的输入数据，以及ChatGPT、Daikon、EvoSpex、Strongarm及Toradocu等工具生成的输出结果。
- Strongarm.ova：预装Strongarm工具的虚拟机镜像，同时包含我们用于测试该工具的示例文件。
- SpecInferenceSurveyArtifact.ova：预装Daikon、EvoSpex及Toradocu工具的虚拟机镜像，同时包含我们用于测试的示例的代码、文档与测试套件。用户可通过该虚拟机自行体验这些规格推断工具。

若仅需获取我们用于测试工具的输入输出数据，则仅使用input-output-examples-for-specification-inference/目录即可满足需求。

许可协议说明
本工件中的工具均遵循其原始许可协议，相关协议文本已随数据集一同提供。
ArrayList.java与Counter.java示例文件遵循CC-BY 4.0许可协议。
BinarySearchGood.java示例文件源自https://www.openjml.org/examples，遵循CC-BY-NC 4.0许可协议共享。