Hoare-Style Verification of Graph Programs

Issue title: Recent Developments in the Theory of Graph Transformation, 2010

Article type: Research Article

Authors: Poskitt, Christopher M. | Plump, Detlef

Affiliations: Department of Computer Science, The University of York, Deramore Lane, York, YO10 5GH, United Kingdom, cposkitt@cs.york.ac.uk; det@cs.york.ac.uk

Note: [] This author is grateful to be supported by a scholarship of the Engineering and Physical Sciences Research Council. Address for correspondence: Department of Computer Science, The University of York, Deramore Lane, York, YO10 5GH, United Kingdom

Abstract: GP (for Graph Programs) is an experimental nondeterministic programming language for solving problems on graphs and graph-like structures. The language is based on graph transformation rules, allowing visual programming at a high level of abstraction. In particular, GP frees programmers from dealing with low-level data structures. In this paper, we present a Hoare-style proof system for verifying the partial correctness of (a subset of) graph programs. The pre- and post-conditions of the calculus are nested graph conditions with expressions, a formalism for specifying both structural graph properties and properties of labels. We show that our proof system is sound with respect to GP's operational semantics and give examples of its use.

DOI: 10.3233/FI-2012-708

Journal: Fundamenta Informaticae, vol. 118, no. 1-2, pp. 135-175, 2012