Elimination of Ghost Variables in Program Logics
Elimination of Ghost Variables in Program Logics
复制标题
消除程序逻辑中的幽灵变量
DOI：
10.1007/978-3-540-78663-4_1
复制
发表时间：
2007
影响因子：
2.9
通讯作者：
M. Pavlova
中科院分区：
文献类型：
--
作者：
M. Hofmann;M. Pavlova
幽灵变量是出现在程序注释中但不对应于物理实体的可赋值变量。它们用于促进规范和验证，例如，通过使用ghost变量来计算循环的迭代次数，并表示额外的功能行为。在本文中，我们给出了一个正式的幽灵变量模型，并展示了它们如何可以从规范和证明中以组合和自动的方式消除。因此，本文的结果，鬼变量可以被看作是一个规范模式，而不是一个原始的概念。
Ghost variables are assignable variables that appear in program annotations but do not correspond to physical entities. They are used to facilitate specification and verification, e.g., by using a ghost variable to count the number of iterations of a loop, and also to express extra-functional behaviours. In this paper we give a formal model of ghost variables and show how they can be eliminated from specifications and proofs in a compositional and automatic way. Thus, with the results of this paper ghost variables can be seen as a specification pattern rather than a primitive notion.