Verifying Graph Programs with First-Order Logic

Gia S. Wulandari
(University of York, UK; Telkom University, Bandung, Indonesia)
Detlef Plump
(University of York, UK)

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.

In Berthold Hoffmann and Mark Minas: Proceedings of the Eleventh International Workshop on Graph Computation Models (GCM 2020), Online-Workshop, 24th June 2020, Electronic Proceedings in Theoretical Computer Science 330, pp. 181–200.
Published: 3rd December 2020.

ArXived at: http://dx.doi.org/10.4204/EPTCS.330.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org