自然语言逻辑：基于自然语言规约逻辑形式对程序进行形式化验证
编程语言
2021-03-11 v1
摘要
形式化验证为软件提供了强有力的正确性保证，这在安全或安全关键系统中尤为重要。Hoare逻辑是一种广泛使用的 formalism，用于对软件针对以前置条件/后置条件断言形式给出的规约进行严格验证。语义解析技术的进步与计算能力的提升，使我们能够从自然语言文本中以日益准确和覆盖度更高的方式提取形式化逻辑形式作为语义内容。本文提出了一种基于Hoare逻辑的形式化验证框架，利用对自然语言断言进行组合语义解析所生成的逻辑形式，对命令式程序进行验证。我们将该推理方法称为自然语言Hoare逻辑（Natural Hoare Logic）。这使得软件能够直接针对领域专家以自然语言指定的安全需求进行形式化验证。我们同时考虑了程序不变式与状态变化的声明式断言，以及指定改变程序状态的命令的命令式断言。我们讨论了如何利用领域知识扩展该推理方法，以及一种防范语义解析器错误的实用途径。
引用
@article{arxiv.2103.05779,
title = {Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications},
author = {Jayaraj Poroor},
journal= {arXiv preprint arXiv:2103.05779},
year = {2021}
}