步进索引模型下的语义及其形式化

Semantics under Step-indexed Model and Formalization

霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.

Hoare logic is the logic base of computer programming. It is used to describe verification of general programs. Separation logic as an extension of Hoare logic, provides supports for high order features used in modern programming languages. Step-indexed model is used to define self-referential predicates. Step-indexed logic is widely used in various program verification tools based on interactive theorem prover, but the reasoning based on step index logic is more complex and complicated than that based on classical logic. On step-indexed model, it is also able to define the non-step-indexed semantics under classical logic system which is more concise and clearer,and independent of the number of steps. Aiming at studying the relationship between stepping index logic and non-stepping index logic, it is found that the two logics are not equivalent. This study summarizes the propositions involved in practical program verification, finds out their common characteristics, and gives the constraint conditions of assertions about program states. The semantics of assertions in step-indexed logic and non-step-indexed logic are defined respectively, and the equivalence of the two semantics is proved under the constraint conditions. All the above definitions and proofs are formalized in Coq. Finally, the future research directions are discussed preliminarily.