将 Hoare 逻辑的证明表转换为重写归纳的推理序列
计算机科学中的逻辑
2018-02-20 v1
摘要
Hoare 逻辑的证明表是带有前置和后置条件的注解程序，对应于 Hoare 逻辑的推理树。在本文中，我们展示可将用于部分正确性的证明表转换为约束重写的重写归纳推理序列。我们还展示，若从程序获得的约束重写系统是终止的，则所得序列是对应于该 Hoare 三元组的归纳定理的有效证明。这种具有约束重写系统终止性的有效证明意味着程序相对于该 Hoare 三元组的总正确性。该转换为我们将证明约束重写终止的技术应用于证明程序总正确性，并结合部分正确性的证明表。
引用
@article{arxiv.1802.06494,
title = {Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction},
author = {Shinnosuke Mizutani and Naoki Nishida},
journal= {arXiv preprint arXiv:1802.06494},
year = {2018}
}
备注
In Proceedings WPTE 2017, arXiv:1802.05862