Evaluation of Specification Inference Tools for Deductive Verification

<strong>About this artifact</strong>As 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.<br>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.<br><strong>License information</strong>The 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.<strong>关于本研究工件</strong>本研究中，我们针对演绎验证（deductive verification）领域的多款规格推断（specification inference）工具，评估了其应用效果与性能表现。本研究工件包含以下内容：<br>- <code>input-output-examples-for-specification-inference/</code>：该目录存放了我们用于测试规格推断工具的输入数据，以及ChatGPT、Daikon、EvoSpex、Strongarm与Toradocu这几款工具生成的输出结果。<br>- <code>Strongarm.ova</code>：预装Strongarm工具的虚拟机（Virtual Machine）镜像，同时包含我们用于测试该工具的示例代码。<br>- <code>SpecInferenceSurveyArtifact.ova</code>：预装Daikon、EvoSpex与Toradocu三款工具的虚拟机镜像，同时包含我们用于测试这些工具的示例代码、配套文档与测试套件。<br>你可通过这些虚拟机镜像自行体验这些规格推断工具。若你仅需获取我们用于测试工具的输入输出数据，则仅需使用<code>input-output-examples-for-specification-inference/</code>目录即可。<br><strong>许可证信息</strong>本工件内的工具均沿用其原始许可证，相关许可证文件已包含在本数据集中。<br><code>ArrayList.java</code>与<code>Counter.java</code>示例代码采用CC-BY 4.0许可证进行授权。<br><code>BinarySearchGood.java</code>示例代码源自https://www.openjml.org/examples，采用CC-BY-NC 4.0许可证进行共享发布。