专为验证失败时辅助人类推理而设计的带特性与验证条件的F-IDE
计算机科学中的逻辑
2021-11-17 v1 软件工程
摘要
本文总结了我们通过所开发的两种不同形式化集成开发环境（F-IDE）在验证失败时辅助人类推理的努力。两种环境均为模块化设计，并有助于对基于对象代码的整体行为进行推理。第一个环境称为web-IDE，多年来一直用于教学形式化规约与验证的各个方面，包括验证条件（VCs）为何及在何处产生，以及验证失败时如何使用它们。第二个F-IDE，RESOLVE Studio，仍处于实验阶段，但是一个更为完备的环境，由基于相继式的VC生成器支撑，可生成具有更少无关给定的VCs。尽管这些环境与VC生成技术必然特定于语言，但替代性VC生成方法、F-IDE特性及其对新手与经验丰富用户影响的相关原则具有更广泛的适用性。
引用
@article{arxiv.2111.08207,
title = {F-IDEs with Features and VCs Designed to Assist Human Reasoning When Verification Fails},
author = {Yu-Shan Sun and Daniel Welch and Murali Sitaraman},
journal= {arXiv preprint arXiv:2111.08207},
year = {2021}
}
备注
In Proceedings AppFM 2021, arXiv:2111.07538