A Hoare Calculus for Graph Programs
Christopher M. Poskitt and Detlef Plump
Department of Computer Science
The University of York, UK
Abstract. We present Hoare-style axiom schemata and inference rules
for verifying the partial correctness of programs in the graph program-
ming language GP. The pre- and postconditions of this calculus are the
nested conditions of Habel, Pennemann and Rensink, extended with ex-
pressions for labels in order to deal with GP’s conditional rule schemata
and infinite label alphabet. We show that the proof rules are sound with
respect to GP’s operational semantics.
1 Introduction
Recent years have seen an increased interest in formally verifying properties
of graph transformation systems, motivated by the many applications of graph
transformation to specification and programming. Typically, this work has fo-
cused on verification techniques for sets of graph transformation rules or graph
grammars, see for example [16,2,10,3,5].
Graph transformation languages and systems such as PROGRES [17], AGG
[18], Fujaba [12] and GrGen [4], however, allow one to use control constructs on
top of graph transformation rules for solving graph problems in practice. The
challenge to verify programs in such languages has, to the best of our knowledge,
not yet been addressed.
A first step beyond the verification of plain sets of rules has been made by
Habel, Pennemann and Rensink in [6], by providing a construction for weakest
preconditions of so-called high-level programs. These programs allow one to use
constructs such as sequential composition and as-long-as-possible iteration over
sets of conditional graph transformation rules. The verification method follows
Dijkstra’s approach to program verification: one calculates the weakest precon-
dition of a program and then needs to prove that it follows from the program’s
precondition. High-level programs fall short of practical graph transformation
languages though, in that their rules cannot perform computations on labels (or
attributes).
In this paper, we present an approach for verifying programs in the graph
programming language GP [13,11]. Rather than adopting a weakest precondition
approach, we follow Hoare’s seminal paper [9] and devise a calculus of proof rules
which are directed by the syntax of the language’s control constructs. Similar to
classical Hoare logic, the calculus aims at human-guided verification and allows
the compositional construction of proofs.

The pre- and postconditions of our calculus are nested conditions [5], ex-
tended with expressions for labels and so-called assignment constraints; we refer
to them as E-conditions. The extension is necessary for two reasons. Firstly,
when a label alphabet is infinite, it is impossible to express a number of simple
properties with finite nested conditions. For example, one cannot express with a
finite nested condition that a graph over the set of integers is non-empty, since
it is impossible to finitely enumerate every integer. Secondly, the conditions in
[5] cannot express relations between labels such as “x and y are integers and
x2 = y”. Such relations can be expressed, however, in GP’s rule schemata.
We briefly review the preliminaries in Section 2 and graph programs in Sec-
tion 3. Following this, we present E-conditions in Section 4, and then use them
to define a proof system for GP in Section 5, where its use will be demonstrated
by proving a property of a graph colouring program. In Section 6, we formally
define the two transformations of E-conditions used in the proof system, before
proving the axiom schemata and inference rules sound in the sense of partial
correctness, with respect to GP’s operational semantics [13,14]. Finally, we con-
clude in Section 7. A long version of this paper with the abstract syntax and
operational semantics of GP, as well as detailed proofs of results, is available
online [15].
2 Graphs, Assignments, and Substitutions
Graph transformation in GP is based on the double-pushout approach with rela-
belling [8]. This framework deals with partially labelled graphs, whose definition
we recall below. We deal with two classes of graphs, “syntactic” graphs labelled
with expressions and “semantic” graphs labelled with (sequences of) integers
and strings. We also introduce assignments which translate syntactic graphs
into semantic graphs, and substitutions which operate on syntactic graphs.
A graph over a label alphabet C is a system G = (VG, EG, sG, tG, lG,mG),
where VG and EG are finite sets of nodes (or vertices) and edges, sG, tG : EG →
VG are the source and target functions for edges, lG : VG → C is the partial node
labelling function and mG : EG → C is the (total) edge labelling function. Given
a node v, we write lG(v) = ⊥ to express that lG(v) is undefined. Graph G is
totally labelled if lG is a total function.
Unlabelled nodes will occur only in the interfaces of rules and are necessary
in the double-pushout approach to relabel nodes. There is no need to relabel
edges as they can always be deleted and reinserted with changed labels.
A graph morphism g : G → H between graphs G and H consists of two
functions gV : VG → VH and gE : EG → EH that preserve sources, targets and
labels; that is, sH ◦ gE = gV ◦ sG, tH ◦ gE = gV ◦ tG, mH ◦ gE = mG, and
lH(g(v)) = lG(v) for all v such that lG(v) 6= ⊥. Morphism g is an inclusion
if g(x) = x for all nodes and edges x. It is injective (surjective) if gV and gE
are injective (surjective). It is an isomorphism if it is injective, surjective and
satisfies lH(gV (v)) = ⊥ for all nodes v with lV (v) = ⊥. In this case G and H
are isomorphic, which is denoted by G ∼= H.

We consider graphs over two distinct label alphabets. Graph programs and
E-conditions contain graphs labelled with expressions, while the graphs on which
programs operate are labelled with (sequences of) integers and character strings.
We consider graphs of the first type as syntactic objects and graphs of the second
type as semantic objects, and aim to clearly separate the levels of syntax and
semantics.
Let Z be the set of integers and Char be a finite set of characters (that can
be typed on a keyboard). We fix the label alphabet L = (Z ∪ Char∗)+ of all
non-empty sequences over integers and character strings, and denote by G(L)
the set of all graphs over L.
The other label alphabet we are using consists of expressions according to
the EBNF grammar of Figure 1, where VarId is a syntactic class1 of variable
identifiers. We write G(Exp) for the set of all graphs over the syntactic class
Exp.
Exp ::= (Term | String) [’ ’ Exp]
Term ::= Num | VarId | Term ArithOp Term
ArithOp ::= ’+’ | ’-’ | ’∗’ | ’/’
Num ::= [’-’] Digit {Digit}
String ::= ’ ” ’ {Char} ’ ” ’
Fig. 1. Syntax of expressions
Each graph in G(Exp) represents a possibly infinite set of graphs in G(L). The
latter are obtained by instantiating variables with values from L and evaluating
expressions. An assignment is a mapping α : VarId→ L. Given an expression e,
α is well-typed for e if for every term t1 ⊕ t2 in e, with ⊕ ∈ ArithOp, we have
α(x) ∈ Z for all variable identifiers x in t1⊕ t2. In this case we inductively define
the value eα ∈ L as follows. If e is a numeral or a sequence of characters, then
eα is the integer or character string represented by e. If e is a variable identifier,
then eα = α(e). Otherwise, if e has the form t1 ⊕ t2 with ⊕ ∈ ArithOp and
t1, t2 ∈ Term, then eα = tα1 ⊕Z tα2 where ⊕Z is the integer operation represented
by ⊕. Finally, if e has the form t e1 with t ∈ Term ∪ String and e1 ∈ Exp, then
eα = tαeα1 (the concatenation of tα and eα1 ).
Given a graph G in G(Exp) and an assignment α that is well-typed for all
expressions occurring in G, we write Gα for the graph in G(L) that is obtained
from G by replacing each label e with eα. If g : G → H is a graph morphism
between graphs in G(Exp), then gα denotes the morphism 〈gαV , gαE〉 : Gα → Hα.
A substitution is a mapping σ : VarId→ Exp. Given an expression e, σ is well-
typed for e if for every term t1⊕ t2 in e, with ⊕ ∈ ArithOp, we have σ(x) ∈ Term
for all variable identifiers x in t1 ⊕ t2. In this case the expression eσ is obtained
from e by replacing every occurrence of a variable x with σ(x). Given a graph G
1 For simplicity, we use the non-terminals of our grammars to denote the syntactic
classes of strings that can be derived from them.

in G(Exp), we write Gσ for the graph that is obtained by replacing each label e
with eσ. If g : G → H is a graph morphism between graphs in G(Exp), then gσ
denotes the morphism 〈gσV , gσE〉 : Gσ → Hσ.
Given an assignment α, the substitution σα induced by α maps every variable
x to the expression that is obtained from α(x) by replacing integers and strings
with their syntactic counterparts. For example, if α(x) is the sequence 56, a, bc ,
where 56 is an integer and a and bc are strings, then σα(x) = 56 ”a” ”bc”.
3 Graph Programs
We briefly review GP’s conditional rule schemata and discuss an example pro-
gram. Technical details (including an operational semantics later used in our
soundness proof) and further examples can be found in [13,14].
3.1 Conditional Rule Schemata
Conditional rule schemata are the “building blocks” of graph programs: a pro-
gram is essentially a list of declarations of conditional rule schemata together
with a command sequence for controlling the application of the schemata. Rule
schemata generalise graph transformation rules in the double-pushout approach
with relabelling [8], in that labels can contain expressions over parameters of
type integer or string. Figure 2 shows a conditional rule schema consisting of the
identifier bridge followed by the declaration of formal parameters, the left and
right graphs of the schema which are graphs in G(Exp), the node identifiers 1,
2, 3 specifying which nodes are preserved, and the keyword where followed by a
rule schema condition.
bridge(a, b, x, y, z : int)
x
1
y
2
z
3
a b
⇒ x
1
y
2 3
z
a+ b
a b
where not edge(1, 3)
Fig. 2. A conditional rule schema
In the GP programming system [11], rule schemata are constructed with a
graphical editor. Labels in the left graph comprise only variables and constants
(no composite expressions) because their values at execution time are determined
by graph matching. The condition of a rule schema is a Boolean expression built
from arithmetic expressions and the special predicate edge, where all variables

occurring in the condition must also occur in the left graph. The predicate edge
demands the (non-)existence of an edge between two nodes in the graph to
which the rule schema is applied. For example, the expression not edge(1, 3) in
the condition of Figure 2 forbids an edge from node 1 to node 3 when the left
graph is matched. The grammar of Figure 3 defines the syntax of rule schema
conditions, where Term is the syntactic class defined in Figure 1.
BoolExp ::= edge ’(’ Node ’,’ Node ’)’ | Term RelOp Term
| not BoolExp | BoolExp BoolOp BoolExp
Node ::= Digit {Digit}
RelOp ::= ’=’ | ’\=’ | ’>’ | ’<’ | ’>=’ | ’<=’
BoolOp ::= and | or
Fig. 3. Syntax of rule schema conditions
Conditional rule schemata represent possibly infinite sets of conditional graph
transformation rules over graphs in G(L), and are applied according to the
double-pushout approach with relabelling. A rule schema L ⇒ R with condi-
tion Γ represents conditional rules 〈〈Lα ← K → Rα〉, Γα,g〉, where K consists
of the preserved nodes (which are unlabelled) and Γα,g is a predicate on graph
morphisms g : Lα → G (see [13,14]).
3.2 Programs
We discuss an example program to familiarise the reader with GP’s features.
This program will be a running example throughout the remainder of the paper.
Example 1 (Colouring). A colouring for a graph is an assignment of colours
(integers) to nodes such that the source and target of each non-looping edge
have different colours. The program colouring in Figure 4 produces a colouring
for every integer-labelled input graph, recording colours as so-called tags. In
general, a tagged label is a sequence of expressions separated by underscores.
The program initially colours each node with 1 by applying the rule schema
init as long as possible, using the iteration operator ’!’. It then repeatedly in-
crements the target colour of edges with the same colour at both ends. Note that
this process is highly nondeterministic: Figure 4 shows an execution producing
a colouring with two colours, but a colouring with three colours could have been
produced for the same input graph.
It is easy to see that whenever colouring terminates, the resulting graph
is a correctly coloured version of the input graph. This is because the output
cannot contain an edge with the same colour at both incident nodes, as then
inc would have been applied at least one more time. Also, it can be shown that
every execution of the program terminates after at most a quadratic number of
rule schema applications [13].

main = init!; inc!
init(x : int)
1
x ⇒
1
x 1
inc(i, k, x, y : int)
x i y i
1 2
k
⇒ x i y i+1
1
2
k
0
0
0
0
0 0
00
+→ 0 1
0 2
0 1
0 2
0 0
00
Fig. 4. The program colouring and one of its executions
4 Nested Graph Conditions with Expressions
We introduce nested graph conditions with expressions (or E-conditions) to
specify graph properties in the pre- and postconditions of graph programs. E-
conditions extend the nested conditions of [5] with expressions for labels, and
assignment constraints which restrict the values that can be assigned to vari-
ables. The resulting conditions can be considered as representations of possibly
infinite sets of ordinary nested conditions.
Definition 1 (Assignment constraint) An assignment constraint is a Bool-
ean expression conforming to the grammar in Figure 5. We require that the
arguments of the operators >, <, ≥ and ≤ belong to the syntactic class Term
and that the arguments of = and 6= belong both to either Term, String or
Exp− (Term ∪ String). (See Figure 1 for the definition of Term, String and Exp.)
Given an assignment constraint γ and an assignment α : VarId → L, the
value γα in B = {tt, ff} is inductively defined2. If γ = true, then γα = tt. If
γ has the form e1 ⊲⊳ e2 with ⊲⊳ ∈ ACRelOp and e1, e2 ∈ Exp, then γα = tt
2 We assume that α is well-typed for γ, which is defined in a similar way to before.

ACBoolExp ::= Exp ACRelOp Exp | ’¬’ ACBoolExp
| ACBoolExp ACBoolOp ACBoolExp
| ’type’ ’(’ VarId ’)’ ’=’ Type | ’true’
ACRelOp ::= ’=’ | ’ 6=’ | ’>’ | ’<’ | ’≥’ | ’≤’
ACBoolOp ::= ’∧’ | ’∨’
Type ::= ’int’ | ’string’ | ’tagged’
Fig. 5. Syntax of assignment constraints
if and only if eα1 ⊲⊳L eα2 where ⊲⊳L is the obvious relation on L represented by
⊲⊳. If γ = ¬γ1 with γ1 ∈ ACBoolExp, then γα = tt if and only if γα1 = ff. If
γ = γ1 ⊕ γ2 with γ1, γ2 ∈ ACBoolExp and ⊕ ∈ ACBoolOp, then γα = γα1 ⊕B γα2
where ⊕B is the Boolean operation on B represented by ⊕. Finally, if γ has the
form type(x) = t with x ∈ VarId and t ∈ Type, then γα = tt if and only if
type(α(x)) = t, where the function type : L → Type is defined by
type(l) =



int if l ∈ Z,
string if l ∈ Char∗,
tagged otherwise.
Example 2 (Assignment constraint). Consider the assignment constraint γ =
a>b ∧ b 6=0 ∧ type(a) = int. Let α1 = (a 7→ 5, b 7→ 1) and α2 = (a 7→ 3, b 7→ 0).
Then γα1 = tt and γα2 = ff.
Note that variables in assignment constraints do not have a type per se, unlike
the variables in GP rule schemata. Rather, the operator ’type’ can be used to
constrain the type of a variable. Note also that an assignment constraint such
as a > 5∧ type(a) = string evaluates under every assignment to ff, because we
assume that assignments are well-typed.
A substitution σ : VarId→ Exp is well-typed for an assignment constraint γ
if the replacement of every occurrence of a variable x in γ with σ(x) results in
an assignment constraint. In this case the resulting constraint is denoted by γσ.
Definition 2 (E-condition) An E-condition c over a graph P is of the form
true or ∃(a|γ, c′), where a : P →֒ C is an injective3 graph morphism with P,C ∈
G(Exp), γ is an assignment constraint, and c′ is an E-condition over C. Moreover,
Boolean formulas over E-conditions over P yield E-conditions over P , that is,
¬c and c1 ∧ c2 are E-conditions over P , where c1 and c2 are E-conditions over
P .
For brevity, we write false for ¬true, ∃(a|γ) for ∃(a|γ, true), ∃(a, c′) for
∃(a|true, c′), and ∀(a|γ, c′) for ¬∃(a|γ,¬c′). In examples, when the domain of
morphism a : P →֒ C can unambiguously be inferred, we write only the codomain
C. For instance, an E-condition ∃(∅ →֒ C, ∃(C →֒ C ′)) can be written as
3 For simplicity, we restrict E-conditions to injective graph morphisms since this is
sufficient for GP.

∃(C, ∃(C ′)), where the domain of the outermost morphism is the empty graph,
and the domain of the nested morphism is the codomain of the encapsulating E-
condition’s morphism. An E-condition over a graph morphism whose domain is
the empty graph is referred to as an E-constraint. We later refer to E-conditions
over left- and right-hand sides of rule schemata as E-app-conditions.
Example 3 (E-condition). The E-condition ∀( x y | x > y, ∃( x y ))
(which is an E-constraint) expresses that every pair of adjacent integer-labelled
nodes with the source label greater than the target label has a loop incident to
the source node. The unabbreviated version of the condition is as follows:
¬∃(∅ →֒ x
1
y
2
| x > y, ¬∃( x
1 2
y →֒
1
x
2
y |true, true)).
The satisfaction of E-conditions by injective graph morphisms over L is de-
fined inductively. Every such morphism satisfies the E-condition true. An in-
jective graph morphism s : S →֒ G with S,G ∈ G(L) satisfies the condition
c = ∃(a : P →֒ C|γ, c′), denoted s |= c, if there exists an assignment α such that
S = Pα and there is an injective graph morphism q : Cα →֒ G with q ◦ aα = s,
γα = tt, and q |= (c′)σα , where σα is the substitution induced by α.
A graph G in G(L) satisfies an E-condition c, denoted G |= c, if the morphism
∅ →֒ G satisfies c.
The application of a substitution σ to an E-condition c is defined inductively,
too. We have trueσ = true and ∃(a|γ, c′)σ = ∃(aσ|γσ, (c′)σ), where we assume
that σ is well-typed for all components it is applied to.
5 A Hoare Calculus for Graph Programs
We present a system of partial correctness proof rules for GP, in the style of Hoare
[1], using E-constraints as the assertions. We demonstrate the proof system by
proving a property of our earlier colouring graph program, and sketch a proof
of the rules’ soundness according to GP’s operational semantics [13,14].
Definition 3 (Partial correctness) A graph program P is partially correct
with respect to a precondition c and a postcondition d (both of which are E-
constraints), if for every graph G ∈ G(L), G |= c implies H |= d for every graph
H in JP KG.
Here, J K is GP’s semantic function (see [14]), and JP KG is the set of all graphs
resulting from executing program P on graph G. Note that partial correctness of
a program P does not entail that P will actually terminate on graphs satisfying
the precondition.
Given E-constraints c, d and a program P , a triple of the form {c} P {d}
expresses the claim that whenever a graph G satisfies c, then any graphs result-
ing from the application of P to G will satisfy d. Our proof system in Figure
6 operates on such triples. As in classical Hoare logic [1], we use the proof sys-
tem to construct proof trees, combining axiom schemata and inference rules (an

example will follow). We let c, d, e, inv range over E-constraints, P,Q over arbi-
trary command sequences, r, ri over conditional rule schemata, and R over sets
of conditional rule schemata.
[rule] {Pre(r, c)} r {c} [ruleset1] {¬App(R)} R {false}
{c} r1 {d} . . . {c} rn {d}
[ruleset2] {c} {r1, . . . , rn} {d}
{inv} R {inv}
[!] {inv} R! {inv ∧ ¬App(R)}
{c} P {e} {e} Q {d}
[comp] {c} P ; Q {d}
{c′} P {d′}
[cons] c =⇒ c′ d′ =⇒ d{c} P {d}
{c ∧App(R)} P {d} {c ∧ ¬App(R)} Q {d}
[if] {c} if R then P else Q {d}
Fig. 6. Partial correctness proof system for GP
Two transformations — App and Pre — are required in some of the asser-
tions. Intuitively, App takes as input a set R of conditional rule schemata, and
transforms it into an E-condition specifying the property that a rule in R is
applicable to the graph. Pre constructs the weakest precondition such that if
G |= Pre(r, c), and the application of r to G results in a graph H, then H |= c.
The transformation Pre is informally described by the following steps: (1) form
a disjunction of right E-app-conditions for the possible overlappings of c and the
right-hand side of the rule schema r, (2) convert the right E-app-condition into
a left E-app-condition (i.e. over the left-hand side of r), (3) nest this within an
E-condition that is quantified over every L and also accounts for the applicability
of r.
Note that two of the proof rules deal with programs that are restricted in
a particular way: both the condition C of a branching command if C then P
else Q and the body P of a loop P ! must be sets of conditional rule schemata.
This restriction does not affect the computational completeness of the language,
because in [7] it is shown that a graph transformation language is complete if
it contains single-step application and as-long-as-possible iteration of (uncondi-
tional) sets of rules, together with sequential composition.
Example 4 (Colouring). Figure 7 shows a proof tree for the colouring pro-
gram of Figure 4. It proves that if colouring is executed on a graph in which

the node labels are exclusively integers, then any graph resulting will have
the property that each node label is an integer with a colour attached to it,
and that adjacent nodes have distinct colours. That is, it proves the triple
{¬∃( a | type(a) 6= int)} init!; inc! {∀( a
1
, ∃( a
1
| a = b c ∧ type(b, c) =
int)) ∧ ¬∃( x i y ik | type(i, k, x, y) = int)}. For conciseness, we abuse our no-
tation (in this, and later examples), and allow type(x1, . . . , xn) = int to represent
type(x1) = int ∧ . . . ∧ type(xn) = int.
[rule] {Pre(init, e)} init {e}
[cons] {e} init {e}
[!] {e} init! {e ∧ ¬App({init})}
[cons] {c} init! {d}
[rule] {Pre(inc, d)} inc {d}
[cons] {d} inc {d}
[!] {d} inc! {d ∧ ¬App({inc})}
[comp] {c} init!; inc! {d ∧ ¬App({inc})}
c = ¬∃( a | type(a) 6= int)
d = ∀( a
1
, ∃( a
1
| a = b c ∧ type(b, c) = int))
e = ∀( a
1
, ∃( a
1
| type(a) = int) ∨ ∃( a
1
| a = b c ∧ type(b, c) = int))
¬App({init}) = ¬∃( x | type(x) = int)
¬App({inc}) = ¬∃( x i y ik | type(i, k, x, y) = int)
Pre(init, e) = ∀( x
1
a
2
| type(x) = int, ∃( x
1
a
2
| type(a) = int)
∨ ∃( x
1
a
2
| a = b c ∧ type(b, c) = int))
Pre(inc, d) = ∀( x i y i a
1 2 3
k | type(i, k, x, y) = int,
∃( x i y i a
1 2 3
k | a = b c ∧ type(b, c) = int))
Fig. 7. A proof tree for the program colouring of Figure 4
6 Transformations and Soundness
We provide full definitions of the transformations App and Pre in this section. In
order to define Pre, it is necessary to first define the intermediary transformations
A and L, which are adapted from basic transformations of nested conditions [5].
Following this, we will show that our proof system is sound according to the
operational semantics of GP.

Proposition 1 (Applicability of a set of rule schemata) For every set R
of conditional rule schemata, there exists an E-constraint App(R) such that for
every graph G ∈ G(L),
G |= App(R)⇐⇒ G ∈ Dom(⇒R),
where G ∈ Dom(⇒R) if there is a direct derivation G⇒R H for some graph H.
The transformation App gives an E-constraint that can only be satisfied by a
graph G if at least one of the rule schemata from R can directly derive a graph H
from G. The idea is to generate a disjunction of E-constraints from the left-hand
sides of the rule schemata, with nested E-conditions for handling restrictions
on the application of the rule schemata (such as the dangling condition when
deleting nodes).
Construction. Define App({}) = false and App({r1, . . . , rn}) = app(r1) ∨
. . . ∨ app(rn). For a rule schema ri = 〈Li ←֓ Ki →֒ Ri〉 with rule schema
condition Γi, define app(ri) = ∃(∅ →֒ Li|γri ,¬Dang(ri) ∧ τ(Li, Γi)) where γri
is a conjunction of expressions constraining the types of variables in ri to the
corresponding types in the declaration of ri. For example, if ri corresponds to
the declaration of inc (Figure 4), then γri would be the Boolean expression
type(i) = int ∧ type(k) = int ∧ type(x) = int ∧ type(y) = int.
Define Dang(ri) =
∨
a∈A ∃a, where the index set A ranges over all4 injective
graph morphisms a : Li →֒ L⊕i such that the pair 〈Ki →֒ Li, a〉 has no natural
pushout5 complement, and each L⊕i is a graph that can be obtained from Li by
adding either (1) a loop, (2) a single edge between distinct nodes, or (3) a single
node and a non-looping edge incident to that node. All items in L⊕i − Li are
labelled with single variables, distinct from each other, and distinct from those
in Li. If the index set A is empty, then Dang(ri) = false.
We define τ(Li, Γi) inductively (see Figure 3 for the syntax of rule schema
conditions). If there is no rule schema condition, then τ(Li, Γi) = true. If Γi has
the form t1 ⊲⊳ t2 with t1, t2 in Term and ⊲⊳ in RelOp, then τ(Li, Γi) = ∃(Li →֒
Li|t1 ⊲⊳ACRelOp t2) where ⊲⊳ACRelOp is the symbol in ACRelOp that corresponds
to the symbol ⊲⊳ from RelOp. If Γi has the form not bi with bi in BoolExp,
then τ(Li, Γi) = ¬τ(Li, bi). If Γi has the form b1 ⊕ b2 with b1, b2 in BoolExp
and ⊕ in BoolOp, then τ(Li, Γi) = τ(Li, b1) ⊕∧,∨ τ(Li, b2) where ⊕∧,∨ is ∧ for
and and ∨ for or. Finally, if Γi is of the form edge(n1,n2) with n1, n2 in Node,
then τ(Li, Γi) = ∃(Li →֒ L′i) where L′i is a graph isomorphic to Li, except for
an additional edge whose source is the node with identifer n1, whose target is
the node with identifier n2, and whose label is a variable distinct from all others
in use.
Proposition 2 (From E-constraints to E-app-conditions) There is a
transformation A such that, for all E-constraints c, all rule schemata r : L⇒ R
4 We equate morphisms with isomorphic codomains, so A is finite.
5 A pushout is natural if is simultaneously a pullback [8].

sharing no variables with c6, and all injective graph morphisms h : Rα →֒ H
where H ∈ G(L) and α is a well-typed assignment,
h |= A(r, c)⇐⇒ H |= c.
The idea of A is to consider a disjunction of all possible overlappings of R and
the graphs of the E-constraint. Substitutions are used to replace label variables
in c with portions of labels from R, facilitating the overlappings.
Construction. All graphs used in the construction of the transformation
belong to the class G(Exp). For E-constraints c = ∃(a : ∅ →֒ C|γ, c′) and rule
schemata r, define A(r, c) = A′(iR : ∅ →֒ R, c). For injective graph morphisms
p : P →֒ P ′, and E-conditions over P ,
A′(p, true) = true,
A′(p, ∃(a|γ, c′)) =
∨
σ∈Σ
∨
e∈εσ
∃(b|γσ,A′(s, (c′)σ)).
P ′ P
C ′
(C ′)σ
C
Cσ
E
(1)
p
a′ a
q
e s
qσ
b
(a′)σ
Construct the pushout (1) of p and a lead-
ing to injective graph morphisms a′ : P ′ →֒ C ′
and q : C →֒ C ′. The finite double disjunc-
tion
∨
σ∈Σ
∨
e∈εσ ranges first over substitu-
tions from Σ, which have the special form
(a1 7→ β1, . . . , ak 7→ βk) where each ai is a dis-
tinct label variable from C that is not also in
P , and each βi is a portion (or the entirety) of
some label from P ′. For each σ ∈ Σ, the dou-
ble disjunction then ranges over every surjec-
tive graph morphism e : (C ′)σ → E such that
b = e ◦ (a′)σ and s = e ◦ qσ are injective graph
morphisms. The set εσ is the set of such sur-
jective graph morphisms for a particular σ, the codomains of which we consider
up to isomorphism. For a surjective graph morphism e1 : (C ′1)σ1 → E1, E1 is
considered redundant and is excluded from the disjunction if there exists a sur-
jective graph morphism, e2 : (C ′2)σ2 → E2, such that E2 ≇ E1, and there exists
some σ ∈ Σ such that Eσ2 ∼= E1.
The transformation A is extended for Boolean formulas over E-conditions in
the same way as transformations over conditions (see [5]).
Example 5. Let r correspond to the rule schema inc (Figure 4), and E-constraint
c = ¬∃( a | type(a) = int). Then,
A(r, c) = ¬∃( x i y i+1k →֒ x i y i+1k a |type(a) = int)
6 It is always possible to replace the label variables in c with new ones that are distinct
from those in r.

Proposition 3 (Transformation of E-app-conditions) There is a transfor-
mation L such that, for every rule schema r = 〈L ←֓ K →֒ R〉 with rule schema
condition Γ , every right E-app-condition c for r, and every direct derivation
G ⇒r,g,h H with g : Lα →֒ G and h : Rα →֒ H where G,H ∈ G(L) and α is a
well-typed assignment,
g |= L(r, c)⇐⇒ h |= c.
Construction. All graphs used in the construction of the transformation be-
long to the class G(Exp). L(r, c) is inductively defined as follows. Let L(r, true) =
true and L(r, ∃(a|γ, c′)) = ∃(b|γ,L(r∗, c′)) if 〈K →֒ R, a〉 has a natural pushout
complement (1) with r∗ = 〈Y ←֓ Z →֒ X〉 denoting the “derived” rule by
constructing natural pushout (2). If 〈K →֒ R, a〉 has no natural pushout com-
plement, then L(r, ∃(a|γ, c′)) = false.
L K R
Y Z X
r :
r∗ :
〈
〈
〉
〉
(1)(2)b a
Example 6. Continuing from Example 5, we get L(r,A(r, c)) = ¬∃( x i y ik →֒
x i y i
k
a |type(a) = int).
Proposition 4 (Transformation of postconditions into preconditions)
There is a transformation Pre such that, for every E-constraint c, every rule
schema r = 〈L ←֓ K →֒ R〉 with rule schema condition Γ , and every direct
derivation G⇒r H,
G |= Pre(r, c) =⇒ H |= c.
Construction. Define Pre(r, c) = ∀(∅ →֒ L|γr, (¬Dang(r) ∧ τ(L, Γ ) =⇒
L(r,A(r, c)))), where γr is as defined in Proposition 1.
Example 7. Continuing from Examples 5 and 6, we get Pre(r, c) = ∀( x i y ik |
type(i, k, x, y) = int,¬∃( x i y ik a |type(a) = int)). Since r does not delete
any nodes, and does not have a rule schema condition, ¬Dang(r)∧τ(L, Γ ) = true,
simplifying the nested E-condition generated by Pre.
Our main result is that the proof rules of Figure 6 are sound for proving
partial correctness of graph programs. That is, a graph program P is partially
correct with respect to a precondition c and a postcondition d (in the sense of
Definition 3) if there exists a full proof tree whose root is the triple {c} P {d}.
Theorem 1. The proof system of Figure 6 is sound for graph programs, in the
sense of partial correctness.

Proof. To prove soundness, we consider each proof rule in turn, appealing to the
semantic function JP KG (defined in [13,14]). The result then follows by induction
on the length of proofs.
Let c, d, e, inv be E-constraints, P,Q be arbitrary graph programs, R be a set
of conditional rule schemata, r, ri be conditional rule schemata, and G,H,G,G′,
H ′ ∈ G(L). → is a small-step transition relation on configurations of graphs and
programs. We decorate the names of the semantic inference rules of [14] with
“SOS”, in order to fully distinguish them from the names in our Hoare calculus.
[rule]. Follows from Proposition 4.
[ruleset1]. Suppose that G |= ¬App(R). Proposition 1 implies that G /∈
Dom(⇒R), hence from the inference rule [Call2]SOS we obtain the transition
〈R, G〉 → fail (intuitively, this indicates that the program terminates but with-
out returning a graph). No graph will ever result; this is captured by the post-
condition false, which no graph can satisfy.
[ruleset2]. Suppose that we have a non-empty set of rule schemata {r1, . . . , rn}
denoted by R, that G |= c, and that we have a non-empty set of graphs
⋃
r∈R{H ∈ G(L)|G ⇒r H} such that each H |= d (if the set was empty, then
[ruleset1] would apply). For the set to be non-empty, at least one r ∈ R must be
applicable to G. That is, there is a direct derivation G⇒R H for some graph H
that satisfies d. From the inference rule [Call1]SOS and the assumption, we get
JRKG = {H ∈ G(L)|〈R, G〉 → H} such that each H |= d.
[comp]. Suppose that G |= c, JP KG = {G′ ∈ G(L)|〈P,G〉 →+ G′} such that
each G′ |= e, and JQKG′ = {H ∈ G(L)|〈Q,G′〉 →+ H} such that each H |= d.
Then JP ; QKG = {H ∈ G(L)|〈P ; Q,G〉 →+ 〈Q,G′〉 →+ H} such that each
H |= d follows from the inference rule [Seq2]SOS.
[cons]. Suppose that G′ |= c′, c =⇒ c′, d′ =⇒ d, and JP KG′ = {H ′ ∈
G(L)|〈P,G′〉 →+ H ′} such that each H ′ |= d′. If G |= c, we have G |= c′ since
c =⇒ c′. The assumption then gives us an H ∈ JP KG such that H |= d′. From
d′ =⇒ d, we get H |= d.
[if]. Case One. Suppose that G |= c, JP KG = {H ∈ G(L)|〈P,G〉 →+ H}
such that each H |= d, and G |= App(R). Then by Proposition 1, executing
R on G will result in a graph. Hence by the assumption and the inference rule
[If1]SOS, Jif R then P else QKG = {H ∈ G(L)|〈if R then P else Q,G〉 →
〈P,G〉 →+ H} such that each H |= d. Case Two. Suppose that G |= c, JQKG =
{H ∈ G(L)|〈Q,G〉 →+ H} such that each H |= d, and G |= ¬App(R). Then
by Proposition 1, executing R on G will not result in a graph. Hence by the
assumption and the inference rule [If2]SOS, Jif R then P else QKG = {H ∈
G(L)|〈if R then P else Q,G〉 → 〈Q,G〉 →+ H} such that each H |= d.
[!]. We prove the soundness of this proof rule by induction over the num-
ber of executions of R that do not result in finite failure, which we denote
by n. Assume that for any graph G′ such that G′ |= inv, JRKG′ = {H ′ ∈
G(L)|〈R, G′〉 →+ H ′} such that each H ′ |= inv. Induction Basis (n = 0). Sup-
pose that G |= inv. Only the inference rule [Alap2]SOS can be applied, that is,
JR!KG = {G ∈ G(L)|〈R!, G〉 → G}. Since the graph is not changed, trivially,
the invariant holds, i.e. G |= inv. Since the execution of R on G does not result

in a graph, G |= ¬App(R). Induction Hypothesis (n = k). Assume that there
exists a configuration 〈R!, G〉 such that 〈R!, G〉 →∗ 〈R!, H〉 → H. Hence for
JR!KG = {H ∈ G(L)|〈R!, G〉 →∗ 〈R!, H〉 → H}, we assume that if G |= inv,
then each H |= inv and H |= ¬App(R). Induction Step (n = k + 1). We have
JR!KG = {H ∈ G(L)|〈R!, G〉 → 〈R!, G〉 →∗ 〈R!, H〉 → H}. Let G |= inv, and
G ∼= G′. From the assumption, we get H ′ |= inv, H ′ ∼= G, and hence G |= inv.
It follows from the induction hypothesis that each H |= inv and H |= ¬App(R).
7 Conclusion
We have presented the first Hoare-style verification calculus for an implemented
graph transformation language. This required us to extend the nested graph
conditions of Habel, Pennemann and Rensink with expressions for labels and
assignment constraints, in order to deal with GP’s powerful rule schemata and
infinite label alphabet. We have demonstrated the use of the calculus for proving
the partial correctness of a highly nondeterministic colouring program, and have
shown that our proof rules are sound with respect to GP’s formal semantics.
Future work will investigate the completeness of the calculus. Also, we intend
to add termination proof rules in order to verify the total correctness of graph
programs. Finally, we will consider how the calculus can be generalised to deal
with GP programs in which the conditions of branching statements and the
bodies of loops can be arbitrary subprograms rather than sets of rule schemata.
Acknowledgements. We are grateful to the anonymous referees for their com-
ments which helped to improve the presentation of this paper.
References
1. Krzysztof R. Apt, Frank S. de Boer, and Ernst-Ru¨diger Olderog. Verification of
Sequential and Concurrent Programs. Springer-Verlag, third edition, 2009.
2. Paolo Baldan, Andrea Corradini, and Barbara Ko¨nig. A framework for the verifica-
tion of infinite-state graph transformation systems. Information and Computation,
206(7):869–907, 2008.
3. De´nes Bisztray, Reiko Heckel, and Hartmut Ehrig. Compositional verification of
architectural refactorings. In Proc. Architecting Dependable Systems VI (WADS
2008), volume 5835 of Lecture Notes in Computer Science, pages 308–333. Springer-
Verlag, 2009.
4. Rubino Geiß, Gernot Veit Batz, Daniel Grund, Sebastian Hack, and Adam M.
Szalkowski. GrGen: A fast SPO-based graph rewriting tool. In Proc. International
Conference on Graph Transformation (ICGT 2006), volume 4178 of Lecture Notes
in Computer Science, pages 383–397. Springer-Verlag, 2006.
5. Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transforma-
tion systems relative to nested conditions. Mathematical Structures in Computer
Science, 19(2):245–296, 2009.

6. Annegret Habel, Karl-Heinz Pennemann, and Arend Rensink. Weakest precon-
ditions for high-level programs. In Proc. International Conference on Graph
Transformation (ICGT 2006), Lecture Notes in Computer Science, pages 445–460.
Springer-Verlag, 2006.
7. Annegret Habel and Detlef Plump. Computational completeness of programming
languages based on graph transformation. In Proc. Foundations of Software Science
and Computation Structures (FOSSACS 2001), volume 2030 of Lecture Notes in
Computer Science, pages 230–245. Springer-Verlag, 2001.
8. Annegret Habel and Detlef Plump. Relabelling in graph transformation. In Proc.
International Conference on Graph Transformation (ICGT 2002), volume 2505 of
Lecture Notes in Computer Science, pages 135–147. Springer-Verlag, 2002.
9. Tony Hoare. An axiomatic basis for computer programming. Communications of
the ACM, 12(10):576–580, 1969.
10. Barbara Ko¨nig and Vitali Kozioura. Towards the verification of attributed graph
transformation systems. In Proc. Graph Transformations (ICGT 2008), volume
5214 of Lecture Notes in Computer Science, pages 305–320. Springer-Verlag, 2008.
11. Greg Manning and Detlef Plump. The GP programming system. In Proc. Graph
Transformation and Visual Modelling Techniques (GT-VMT 2008), volume 10 of
Electronic Communications of the EASST, 2008.
12. Ulrich Nickel, Jo¨rg Niere, and Albert Zu¨ndorf. The FUJABA environment. In
Proc. International Conference on Software Engineering (ICSE 2000), pages 742–
745. ACM Press, 2000.
13. Detlef Plump. The graph programming language GP. In Proc. Algebraic Informat-
ics (CAI 2009), volume 5725 of Lecture Notes in Computer Science, pages 99–122.
Springer-Verlag, 2009.
14. Detlef Plump and Sandra Steinert. The semantics of graph programs. In Proc.
Rule-Based Programming (RULE 2009), volume 21 of Electronic Proceedings in
Theoretical Computer Science, pages 27–38, 2010.
15. Christopher M. Poskitt and Detlef Plump. A Hoare calcu-
lus for graph programs (long version), 2010. Available online:
http://www.cs.york.ac.uk/plasma/publications/pdf/PoskittPlump.ICGT.10.Long.pdf.
16. Arend Rensink, A´kos Schmidt, and Da´niel Varro´. Model checking graph trans-
formations: A comparison of two approaches. In Proc. Graph Transformations
(ICGT 2004), volume 3256 of Lecture Notes in Computer Science, pages 226–241.
Springer-Verlag, 2004.
17. Andy Schu¨rr, Andreas Winter, and Albert Zu¨ndorf. The PROGRES approach:
Language and environment. In H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozen-
berg, editors, Handbook of Graph Grammars and Computing by Graph Transfor-
mation, volume 2, chapter 13, pages 487–550. World Scientific, 1999.
18. Gabriele Taentzer. AGG: A graph transformation environment for modeling and
validation of software. In Applications of Graph Transformations With Industrial
Relevance (AGTIVE 2003), Revised Selected and Invited Papers, volume 3062 of
Lecture Notes in Computer Science, pages 446–453. Springer-Verlag, 2004.