Hoare Logics for Time Bounds - A Study in Meta Theory
Hoare Logics for Time Bounds - A Study in Meta Theory
复制标题
时间界限的霍尔逻辑 - 元理论研究
DOI：
10.1007/978-3-319-89960-2_9
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Tobias Nipkow
中科院分区：
文献类型：
--
作者：
Maximilian Paul Louis Haslbeck;Tobias Nipkow
我们研究了三种不同的霍尔逻辑，用于推理命令式程序的时间限制，并在 Isabelle/HOL 中将它们形式化：Nielson 提出的经典霍尔逻辑，Carbonneauxet 等人提出的具有潜力的逻辑，以及 Atkey、Chaguérand 和 Pottier 的分离逻辑。这些逻辑被正式证明是合理和完整的。验证条件生成器已开发出来，并且也显示出健全和完整。我们还考虑了系统的变体，在这些变体中，我们从运行时间范围内的乘法常数中抽象出来，从而支持大 O 风格的推理。最后我们比较了三个系统的表达能力。
We study three different Hoare logics for reasoning about time bounds of imperative programs and formalize them in Isabelle/HOL: a classical Hoare like logic due to Nielson, a logic with potentials due to Carbonneauxet al.and aseparation logicfollowing work by Atkey, Chaguérand and Pottier. These logics are formally shown to be sound and complete. Verification condition generators are developed and are shown sound and complete too. We also consider variants of the systems where we abstract from multiplicative constants in the running time bounds, thus supporting a big-O style of reasoning. Finally we compare the expressive power of the three systems.
登录
查看更多内容
霍尔逻辑和辅助变量
影响因子：
1
作者：
["Thomas Kleymann
通讯作者：
["Thomas Kleymann
用于摊销堆空间分析的自动类型推断
DOI：
10.1007/978-3-642-37036-6_32
发表时间：
2013
期刊：
影响因子：
--
作者：
Martin Hofmann;Dulma Rodriguez
通讯作者：
Dulma Rodriguez
DOI：
10.1016/0167-6423(87)90029-3
发表时间：
1987
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
H. R. Nielson
通讯作者：
H. R. Nielson
具有分离逻辑的摊销资源分析
影响因子：
0.6
作者：
Atkey R
通讯作者：
Atkey R
DOI：
--
发表时间：
2007
期刊：
Undergraduate Topics in Computer Science
影响因子：
--
作者：
H. R. Nielson;F. Nielson
通讯作者：
F. Nielson