Mechanizing programming logics in higher order logic
Mechanizing programming logics in higher order logic
复制标题
DOI：
10.1007/978-1-4612-3658-0_10
复制
发表时间：
1989-05
期刊：
影响因子：
--
通讯作者：
M. Gordon
中科院分区：
文献类型：
--
作者：
M. Gordon
关于计算机程序的形式推理可以直接基于编程语言的语义，或者在像霍尔逻辑这样的特殊目的逻辑中完成。第一种方法的优点是，它保证了形式推理适用于所使用的语言（众所周知，例如，Hoare的赋值公理不适用于大多数编程语言）。第二种方法的优点是证明可以更直接和自然。在本文中，我们试图得到这两种方法的优点。霍尔逻辑的规则是机械地从一个简单的命令式编程语言（使用霍尔系统）的语义派生出来的。这些规则构成了一个简单程序验证器的基础，在这个程序验证器中，验证条件是由lcf风格的策略生成的，这些策略的验证使用派生的Hoare规则。因为Hoare逻辑是推导出来的，而不是假设出来的，所以将语义推理和公理推理混合起来是很简单的。将Hoare逻辑的构造与其他特定于应用程序的符号结合起来也很简单。简要说明了各种逻辑构造，包括终止语句、vdm风格的“关系”正确性规范、最弱前提语句和动态逻辑公式。这里介绍的工作背后的理论是众所周知的。我们的贡献是提出一种使这一理论机械化的方法，使某些实际细节顺利地进行。
Formal reasoning about computer programs can be based directly on the semantics of the programming language, or done in a special purpose logic like Hoare logic. The advantage of the first approach is that it guarantees that the formal reasoning applies to the language being used (it is well known, for example, that Hoare’s assignment axiom fails to hold for most programming languages). The advantage of the second approach is that the proofs can be more direct and natural.In this paper, an attempt to get the advantages of both approaches is described. The rules of Hoare logic aremechanicallyderived from the semantics of a simple imperative programming language (using the HOL system). These rules form the basis for a simple program verifier in which verification conditions are generated by LCF-style tactics whose validations use the derived Hoare rules. Because Hoare logic is derived, rather than postulated, it is straightforward to mix semantic and axiomatic reasoning. It is also straightforward to combine the constructs of Hoare logic with other application-specific notations. This is briefly illustrated for various logical constructs, including termination statements, VDM-style ‘relational’ correctness specifications, weakest precondition statements and dynamic logic formulae.The theory underlying the work presented here is well known. Our contribution is to propose a way of mechanizing this theory in a way that makes certain practical details work out smoothly.