A Hoare-Like Proof System for Analysing the Computation Time of Programs
A Hoare-Like Proof System for Analysing the Computation Time of Programs
复制标题
分析程序计算时间的类霍尔证明系统
DOI：
10.1016/0167-6423(87)90029-3
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
H. R. Nielson
中科院分区：
文献类型：
--
作者：
H. R. Nielson
Hoare逻辑的版本已经被引入来证明程序的部分正确性和完全正确性。在本文中，它是如何Hoare证明系统，而程序可以扩展到证明计算时间的属性。应该强调的是，系统不需要通过在时钟变量上插入显式操作来修改程序。我们推广的概念，算术健全和完整的证明系统满足这些。同时，我们推导出了与非正式规则相对应的形式规则，用于确定while程序的计算时间。证明系统的适用性说明了一个例子，气泡排序算法。
Versions of Hoare logic have been introduced to prove partial and total correctness properties of programs. In this paper it is shown how a Hoare-like proof system for while programs may be extended to prove properties of the computation time as well. It should be stressed that the system doesnotrequire the programs to be modified by inserting explicit operations upon a clock variable. We generalize the notions of arithmetically sound and complete and show that the proof system satisfies these. Also we derive formal rules corresponding to the informal rules for determining the computation time of while programs. The applicability of the proof system is illustrated by an example, the bubble sorting algorithm.