TY - JOUR
T1 - Hoare-Style Verification of Graph Programs
AU - Poskitt, Christopher M.
AU - Plump, Detlef
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84862991423&partnerID=8YFLogxK
UR - http://www.cs.york.ac.uk/plasma/publications/pdf/PoskittPlump.FundInf.12.pdf
U2 - 10.3233/FI-2012-708
DO - 10.3233/FI-2012-708
M3 - Article
SN - 0169-2968
VL - 118
SP - 135
EP - 175
JO - Fundamenta Informaticae
JF - Fundamenta Informaticae
IS - 1-2
ER -