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.
翻译:我们考虑Hoare 式的图形编程语言 GP 2. 在先前的工作中,图形属性是由所谓的电子条件确定的,这些条件延长了嵌套的图形条件。 但是,这种类型的断言不容易被程序员理解,而程序员在标准一阶逻辑中用于正式的规格。 在本文中,我们提出一种方法,用标准一阶逻辑来核查GP 2程序。我们展示了如何在规则模式和前提条件方面建立一个最强有力的自由后设条件。 然后我们扩展了这一构思,以获得任意无环程序最有力的自由后设条件。 与先前的工作相比, 这可以解释一个非常广泛的图表程序类别。 特别是, 许多嵌入循环程序可以通过新的计算来验证 。