关于传值调用的推理：霍尔逻辑史中缺失的一个结果
计算机科学中的逻辑
2019-09-16 v1 编程语言
摘要
我们提供了一个可靠且相对完备的类霍尔证明系统，用于在存在局部变量和传值调用参数机制的情况下推理递归过程的部分正确性，并且其中正确性证明在程序长度上是线性的。我们认为，尽管用于递归过程的类霍尔证明系统已被深入研究，但文献中尚未提出过这样的证明系统。
引用
@article{arxiv.1909.06215,
title = {Reasoning about call-by-value: a missing result in the history of Hoare's logic},
author = {Krzysztof R. Apt and Frank S. de Boer},
journal= {arXiv preprint arXiv:1909.06215},
year = {2019}
}
备注
28 pages