论文标题
用一阶逻辑验证图形程序
Verifying Graph Programs with First-Order Logic
论文作者
论文摘要
我们考虑了图形编程语言GP 2的HOARE风格验证。在先前的工作中，通过所谓的电子条件指定了图形属性，这些电子条件扩展了嵌套的图条件。但是，这种类型的断言并不容易理解用于标准一阶逻辑中正式规格的程序员。在本文中，我们提出了一种使用标准一阶逻辑验证GP 2程序的方法。我们展示了如何在规则架构和前提条件方面构建最强的自由邮政编码。然后，我们扩展了这一构造，以获得无循环计划的最强大的自由邮政编码。与以前的工作相比，这允许对大量概括的图形程序进行推理。特别是，许多具有嵌套回路的程序可以通过新的演算进行验证。
We consider Hoare-style verification for the graph programming language GP 2. In previous work, graph properties were specified by so-called E-conditions which extend nested graph conditions. However, this type of assertions is not easy to comprehend by programmers that are used to formal specifications in standard first-order logic. In this paper, we present an approach to verify GP 2 programs with a standard first-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain strongest liberal postconditions for arbitrary loop-free programs. Compared with previous work, this allows to reason about a vastly generalised class of graph programs. In particular, many programs with nested loops can be verified with the new calculus.
