Publication Type
Journal Article
Version
publishedVersion
Publication Date
3-2012
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 postconditions 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.
Discipline
Graphics and Human Computer Interfaces | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Fundamenta Informaticae
Volume
118
Issue
1-2
First Page
135
Last Page
175
ISSN
0169-2968
Identifier
10.3233/FI-2012-708
Publisher
IOS Press
Citation
POSKITT, Christopher M. and PLUMP, Detlef.
Hoare-style verification of graph programs. (2012). Fundamenta Informaticae. 118, (1-2), 135-175.
Available at: https://ink.library.smu.edu.sg/sis_research/4859
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.3233/FI-2012-708