=Paper=
{{Paper
|id=Vol-1403/paper8
|storemode=property
|title=On Correctness of Graph Programs Relative to Recursively Nested Conditions
|pdfUrl=https://ceur-ws.org/Vol-1403/paper8.pdf
|volume=Vol-1403
|dblpUrl=https://dblp.org/rec/conf/gg/Flick15
}}
==On Correctness of Graph Programs Relative to Recursively Nested Conditions==
https://ceur-ws.org/Vol-1403/paper8.pdf
On Correctness of Graph Programs
Relative to Recursively Nested Conditions
Nils Erik Flick⋆
Carl von Ossietzky Universität, 26111 Oldenburg, Germany,
flick@informatik.uni-oldenburg.de
Abstract. We propose a new specification language for the proof-based
approach to verification of graph programs by introducing µ-conditions
as an alternative to existing formalisms which can express path proper-
ties. The contributions of this paper are the lifting of constructions from
nested conditions to the new, more expressive conditions, and a proof
calculus for partial correctness relative to µ-conditions.
1 Introduction
Graph transformations provide a formal way to model the graph-based behaviour
of a wide range of systems by way of diagrams. Such systems can be formally
verified. One approach to verification proceeds via model checking of abstrac-
tions, notably Gadducci et al., Baldan et al., König et al., Rensink et al. [4, 1, 10,
18]. This can be contrasted with the proof-based approaches of Habel, Penne-
mann and Rensink [7, 6] and Poskitt and Plump [15]. Here, state properties are
expressed by nested graph conditions, and a program can be proved correct with
respect to a precondition c and a postcondition d. The following figure presents
a schematic overview of the approach, which is also our starting point:
graph program weakest precondition
precondition
c (precondition) calculus
prover
yes, correct
d (postcondition) no
unknown
The correctness proof is done in the style of Dijkstra’s [2] predicate trans-
former approach in Pennemann’s thesis [12], while Poskitt’s thesis [14] features
a Hoare [8] logic for partial and total correctness. Both works are based on
nested conditions, which cannot express non-local properties of graphs, such as
connectivity. In this paper, we consider non-local properties, and we present an
extension to the proof calculus from [12].
⋆
This work is supported by the German Research Foundation (DFG), grant GRK
1765 (Research Training Group – System Correctness under Adverse Conditions)
Our formalism is an extension of nested conditions by recursive definitions. While
several extensions of nested graph conditions to non-local conditions already
exist (Radke [17], Poskitt and Plump [16]), we argue that as opposed to the
former, ours already offers a weakest precondition calculus that can handle any
condition expressible in it; as compared to the latter, which relies more heavily
on expressing properties directly in (monadic second-order) logic, ours is more
closely related to nested conditions and shares the same basic methodology.
Therefore µ-conditions, albeit still work in progress, offer a new viewpoint that
may be sufficiently different from existing ones to be worth investigating.
The outline of the paper is as follows: Section 2 recalls graph programs and
conditions. Sections 3 and 4 introduce µ-conditions and correctness under µ-
conditions, respectively, together with an exemplary application of the method,
Section 5 provides context by listing related work and Section 6 concludes with
an outlook. After the main text, there is an appendix with the proofs.
2 Graph Conditions and Programs
In this section, we introduce graph conditions and graph programs. We assume
familiarity with graph transformation systems in the sense of Ehrig et al. [3], and
the basic notions of category theory. For standard definitions and more details,
we refer the reader to Ehrig et al. [3]. For an in-depth introduction to nested con-
ditions and graph programs and practical approaches to semi-automatic theorem
proving in this context, we refer the reader to Pennemann [12].
Notation. The domain and codomain of a morphism f : G → H are denoted
by dom(f ) = G and cod(f ) = H. Injective morphisms (monomorphisms) are
distinguished typographically by a curly arrow f : G ֒→ H while double-tailed
arrows f : G ։ H denote surjective ones (epimorphisms). We use the symbol
M to denote the class of all graph monomorphisms. A partial morphism is a pair
of monomorphisms with the same domain. The empty graph is denoted by ∅.
All graphs in this paper are assumed to be finite.
A brief review of nested conditions follows. Nested graph conditions were pro-
posed by Habel and Pennemann. Finite nested conditions were later shown to
be equally expressive as graph-interpreted first-order predicate logic. Graph con-
ditions can be used as constraints to specify state properties, or as application
conditions to restrict the applicability of a rule.
Definition 1 (Nested Graph Conditions). Let Cond be the class of nested
conditions, defined inductively as follows (where P, C ′ , C are graphs):
W J is a countable set and for all j ∈ J, cj is a condition (over P ), then
– If
j∈J cj is a condition (over P ). This includes the case J = ∅ (for any P ).
– If c is a condition (over P ), then ¬c is also a condition (over P ).
– If a : P ֒→ C ′ is a monomorphism, ι : C ֒→ C ′ is a monomorphism and c′ is
a condition (over C), then ∃(a, ι, c′ ) is a condition (over P ).
We call c′ a direct subcondition of ∃(α, ι, c′ ), ¬c′ and c′ ∨c′′ and use subcondition
for the reflexive and transitive closure of this syntactically defined relation.
Notation. If c is a condition over P , then P is its type1 and we write c : P ,
and CondP is the class of all conditions over P . We may write ∃(a, c) instead V of
∃(a, W
idcod(a) , c). The usual abbreviations define the other standard operators:
is ¬ ¬, ∀ is ¬∃¬. No morphism satisfies the disjunction over the empty index
set. We introduce false as a notation for it, and true for ¬false. We may omit
the subcondition true (together with ι), writing ∃(a) for ∃(a, ι, true).
When all the index sets are finite, one obtains the finite nested conditions. The
morphism ι serves to unselect2 a part of C ′ , which will become necessary later.
Definition 2 (Satisfaction). A monomorphism f : P ֒→ G satisfies W a condi-
tion c : P , denoted f |= c, iff c = true, c = ¬c′ and f 6|= c′ , or c = j∈J cj and
there is a j ∈ J such that f |= cj , or c = ∃(a, ι, c′ ) (a : P ֒→ C ′ , ι : C ֒→ C ′ ,
c′ : C) and there exists a monomorphism q : C ′ ֒→ G such that f = q ◦ a and
q ◦ ι |= c′ .
a ι
∃(P C′ C, c′ )
f q |=
q◦ι
G
A graph G satisfies a condition c : ∅ iff the unique morphism ∅ ֒→ G satisfies c.
In the diagram of Def. 2, the triangle indicates that C is the type of the subcon-
dition c′ which appears nested inside ∃(α, ι, c′ ).
Remark 1 (No Added Expressivity). Our conditions with ι are equally expres-
sive as the nested conditions defined in [12]. The proof, which we omit here,
relies on the transformation A from [12].
Definition 3. ≡ denotes logical equivalence, i.e. for conditions c, c′ : P , c ≡ c′
iff for all monomorphisms m with domain P , ⇒ m |= c ⇔ m |= c′ .
Notation. As one can see in Fig. 1, the notation for graph conditions custom-
arily only depicts source or target graphs of morphisms. The tiny blue numbers
1
when we mention “type graphs” in the text, we just mean graphs used as types.
2
We will use the term “unselection” anytime a morphism is used in the inverse direc-
tion: in Def. 1, the morphism ι is used to base subconditions on a smaller subgraph,
in effect reducing the selected subgraph; it will also appear in our definition of graph
programs as the name of an operation that reduces the current selection, i.e. the
subgraph the program is currently working on – similarly for “selection”.
1 2 2 2
|= ∃ ←֓ , ¬∃
Fig. 1. A nested graph condition (stating the existence of two nodes linked by an edge,
where the second node does not have a self-loop) and a graph satisfying it.
show the morphisms’ node mappings. We also adopt the convention of not explic-
itly representing the morphism ι in a situation ∃(a, ι, xi ); we prefer to annotate
the variable’s type graph with the images of items under ι in parentheses.
Next, we introduce graph transformations. We follow the double pushout ap-
proach with injective rules and injective matches. For technical reasons, we de-
fine graph transformations in terms of four elementary steps, namely selection,
deletion, addition and unselection. Deletion and addition always apply to a se-
lected subgraph, and selection and unselection allow the selection to be changed.
skip is a no-op used in the definition of sequential composition. The definition
below allows for somewhat more general combinations of the basic steps, which
cannot be expressed by sets of graph transformation rules.
The semantics of a graph program is a triple of two monomorphisms and one
partial morphism. The two monomorphisms represent the selected subgraphs
before and after the execution of the program respectively, and the partial mor-
phism records the changes effected by the program. Our programs are a proper
subset of those in Pennemann [12], and use the same semantics.
Definition 4 (Graph Programs).
In the following table, x, l, r, y, min and mout are monomorphisms, with x, l, r
and y arbitrarily chosen to define a program step, while min and mout are called
interfaces and universally quantified in the set comprehensions that appear in
the definitions below.
Name Program P Semantics JP K
selection Sel(x) {(min , mout , x) | mout ◦ x = min }
deletion Del(l) {(min , mout , l−1 ) | ∃l′ , (mout , l, min , l′ ) pushout}
addition Add(r) {(min , mout , r) | ∃r′ , (min , r, mout , r′ ) pushout}
unselection U ns(y) {(min , mout , y −1 ) | mout = min ◦ y}
skip skip {(m, m, iddom(m) ) | m ∈ M}
If P and Q are graph programs, then so are their disjunctive {P, Q} and sequen-
tial (P ; Q) composition. The semantics of disjunction is a set union JP K ∪ JQK
and the semantics of sequence is JP ; QK = {(m, m′ , p) | ∃(m, m′′ , p′ ) ∈ JP K,
(m′′ , m′ , p′′ ) ∈ JQK, p = p′ ; p′′ }, where composition p′ ; p′′ of partial morphisms
l1 r1 l2 r2 l1 ◦l2′ r2 ◦r1′
p′ = G1 ←֓ D1 ֒→ H1 , p′′ = H1 ←֓ D2′ ֒→ H2 is defined as G ←֓ D′′ ֒→ H2
′ ′
using the pullback (rS
1 , l2 ) of (r1 , l2 ). If P is a graph program, then so is its
iteration P ; JP K = j∈N JP j K where P j = P ; P j−1 for j ≥ 1 and P 0 = skip.
∗ ∗
Remark 2. The definitions generalise the state transitions in plain graph trans-
l r
formation, a rule ̺ = (L ←֓ K ֒→ R) being precisely simulated by the program
Sel(∅ ֒→ L); Del(l); Add(r); U ns(∅ ֒→ R).
3 µ-Conditions
In this section, we define µ-conditions on the basis of nested graph conditions.
These are capable of expressing path and connectivity properties, which fre-
quently arise in the study of the correctness of programs with recursive data
structures, or in the modelling of networks. We then define and prove the cor-
rectness of some basic constructions. An example is provided at the end of this
section to illustrate the constructions step by step.
3.1 Defining µ-Conditions
Nested conditions are a very successful approach to the specification of graph
properties for verification. However, they are unable to express non-local prop-
erties such as connectedness. Our idea is to generalise nested conditions to cap-
ture certain non-local properties by adding recursion. The resulting formalism
will be similar to first order fixed point logics, see e.g. Kreutzer [9]. The reader
might want to compare our µ-conditions to a distinct formalism towards ex-
pressing non-local properties, the very powerful grammar-based HR∗ conditions
of Radke [17]. We argue that µ-conditions are worth looking into despite the
availability of strong contenders for the extension of nested conditions to non-
local properties, such as MSO-conditions [16] because µ-conditions provide a
new and different generalisation of nested conditions, and neither is it immedi-
ately clear how the respective expressivities compare. The related work section,
Sec. 5, contains a summary on different non-local graph condition formalisms.
Specifically, we will show in this section that the weakest liberal precondition
transformation, core of the Dijkstra-style approach, can be adapted.
Notation. Sequences (of graphs, placeholders, morphisms) are written as bold
letters P , x, f , and their components are numbered starting from 1. The length
of a sequence P is denoted by kP k. Indexed typewriter letters x1 stand for
placeholders, i.e. variables. The notation c : P indicating that c has type P is
also extended to sequences: c : P (provided kck= kP k).
To define fixed point conditions, we need something to take fixed points of, and
to ascertain that the fixed point exists. Choosing a partial order on CondP , one
can define monotonic operators on CondP . The semantics of satisfaction already
defines a pre-order: c ≤ c′ iff every morphism that satisfies c also satisfies c′ ,
which is obviously transitive and reflexive. As in every pre-order, ≤ ∩ ≤−1 is
an equivalence relation compatible with ≤ and comparing representants via ≤
partially orders its equivalence classes. We introduce variables as placeholders
where further conditions can be substituted3 .
3
Note that in our approach variables stand only for subconditions, not for attributes
or parts of graphs. Wherever confusion with similarly named concepts from the
literature could arise, we will use the word “placeholder” meaning “variable”.
To represent systems of simultaneous equations, we work on tuples of conditions.
If P = P1 , . . . , PkP k is a sequence of graphs, then CondP is the set of all kP k-
tuples c of conditions, whose i-th element is a condition over the i-th graph of
P . Satisfaction is defined component-wise: f |= c iff ∀k ∈ {1, . . . , kP k} fk |= ck .
V W
By definition, and of countable sets of CondP conditions exist for any P ,
and they are easily seen to be least upper and greatest lower bounds of the
sets. This makes Cond≡P a complete lattice. Let CondP be ordered with the
product order by defining f |= c to be true when the conjunction holds. This
again induces a partial order on the set of equivalence classes, Cond≡P . Thus,
Cond≡P is also a complete lattice, and monotonic operators have least fixed
points by the Knaster-Tarski theorem [20], given by the limit of F n (false) for
all n ∈ N . This ensures that systems of equations as defined below yield least
fixed point solutions, which is crucial in the definition of a µ-condition. We
extend the inductive definition from Def. 1 as follows:
Definition 5 (Graph Conditions with Placeholders). Given a graph P
and a finite sequence P of graphs or morphisms, a condition with placeholders
W P over P is a (graph) condition with placeholders is either ∃(a, ι, c), or ¬c,
from
or j∈J cj , or xi , 1 ≤ i ≤ kP k where xi is a variable of type Pi .
A condition can be substituted for a variable of same type:
Definition 6 (Substitution). If P is a list of graphs and F is a condition
with placeholders x over P , then if c ∈ CondP , then F[x/c] is obtained by
substituting each occurrence of xi by ci for all i ∈ {1, ..., kPk}.
Satisfaction of conditions with placeholders by a morphism f is defined in the
obvious way relative to a valuation, which is an assignment of true or false to
each monomorphism of the type graph of the variable into cod(f ).
As discussed above, a least fixed point will be sought only up to logical equiv-
alence. To guarantee existence of the least fixed point, the operator must be
monotonic (c ≤ d ⇒ F (c) ≤ F (d) for any c, d ∈ CondP ). Monotonicity can be
enforced syntactically for substitutions by never placing a variable under an odd
number of negations, which is proved by structural induction as in fixed point
logics or the modal µ calculus.
Definition 7 (µ-Condition). Given a finite list P , if {Fi }i∈{1,...,kP k} are con-
ditions with placeholders from P , over the graphs of P respectively, then µ[P ]F
denotes the least fixed point of the operator c 7→ F [x/c].
A µ-condition is a pair (b, l) consisting of a condition with placeholders b, and a
finite list of pairs l = (xi , Fi (x)) of a variable xi : Pi and a condition Fi (x) : Pi ,
with placeholders from x, for some graph Pi , such that F is monotonic.
Notation. we write the list of pairs l = (xi , Fi (x)) as a system of equations
x = F (x). We call b the main body and l the recursive specification of (b, l), and
F (c) is understood as substitution of conditions c for the variables x.
Thus each condition with placeholders typed over P defines a unary operator
on CondP .
Remark 3 (First Example: µ-Conditions are More General than Nested).
1. µ-conditions generalise nested conditions, consequently all examples for nest-
ed conditions are examples for µ-conditions (with no variables or equations).
2. µ-conditions are strictly more general than nested conditions: the following
expresses the existence of a path of unknown length between two given nodes.
3
x1 [ ] where x1 [ ] = ∃( ) ∨ ∃( , x1 [ ])
1 2 1 2 1 2 1 2 1(3) 2(2)
It is read as follows: the word “where” separates the main body from the equa-
tions. Here, x1 is the only variable, and its type graph is indicated in square
brackets. The second existential quantifier uses a morphism to unselect node 1
and the sole edge: its source is the type graph of x1 , which is indeed syntacti-
cally required for using the variable in that place. The unselection morphism ι
is implicit in the notation, and is only expressed by adding small blue numbers
in parentheses to the node numbers in its source graph to specify the mapping.
This compact notation for ι is why the second existential quantifier in the ex-
ample has only two fields. To ease reading and writing, we adopt the convention
to always use precisely the same layout for the type graph of a given variable.
The following statement is not needed in the proofs that will follow, but it helps
motivate the use of the “unselection” morphisms. We therefore view it as justified
to leave the proof as an exercise:
Remark 4 (Why ι). A µ-condition where ι is the identity in all subconditions of
the main body and of the components Fi (x) is equivalent to a nested condition.
The following fact is well-known:
W n
Remark 5. The least fixed point of F is equivalent to n∈N F (false).
Definition 8 (Satisfaction). The µ-condition b | x = F (x) with x : P is
satisfied by a morphism f iff f |= b[x/µ[P]F].
Remark 6 (No Infinite Nesting). By the characterisation of the least fixed point
as an infinite disjunction, every µ-condition is equivalent to an infinite nested
condition. Infinitely deep nesting does not arise, because the characterisation in
Remark 5 yields a countable disjunction of finitely deeply nested conditions.
A morphism satisfies a given µ-condition iff it satisfies the finite nested condition
obtained by unrolling the recursive specification up to some finite depth and
substituting the resulting nested conditions into the main body:
Proposition 1 (Satisfaction at Finite Recursion Depth). f |= b | x =
F (x) iff ∃n ∈ N, f |= b[x/F n (false)].
Theorem 1 (Deciding Satisfaction of µ-conditions). Given a morphism
f : P ֒→ G and a µ-condition c, it is decidable whether f |= c.
3.2 Weakest Liberal Preconditions of µ-conditions
In this subsection, we present a construction to compute the weakest liberal
precondition of any given µ-condition with respect to any graph program P that
does not use iteration (“liberal” means that termination of P is not implied, and is
redundant in the absence of iteration, as only iteration causes non-termination).
Definition 9 (Weakest Liberal Precondition). The weakest liberal precon-
dition (wlp) of c with respect to the program P , wlp(P, c), is the least condition
with respect to implication such that f ′ |= c ⇒ f |= wlp(P, c) if (f, f ′ , p) ∈ JP K
for some partial morphism p.
We will show that under this assumption there is a µ-condition that expresses
precisely the weakest liberal precondition of a given µ-condition with respect to
a rule, and it can be computed. The result is similar to the situation for nested
conditions. To derive it, we use the shift transformation Am (c) from [12] whose
fundamental property is to transform any nested condition c into another nested
condition such that m′′ |= Am (c) iff m′′ ◦ m |= c for all composable pairs m′′ , m
of monomorphisms (Lemma 5.4 from [12]). Since this and similar constructions
play an important role in this section, we recall here the case c = ∃(a, c′ ): if
(m′ , a′ ) is the pushout of (m, a), let Epi be the set of all epimorphisms e with
domain cod(m′ ) thatWcompose to monomorphisms b := e ◦ a′ and r := e ◦ m′ .
Then Am (∃(a, c′ )) = e∈Epi ∃(b, Ar (c′ )).
With help of the unselection ι in ∃(a, ι, c), it is at first glance trivial to exhibit
a weakest liberal precondition with respect to U ns(y). However, to handle the
addition and deletion steps, a construction becomes necessary that makes the
affected subgraph explicit again. This information is crucial to obtain the weakest
liberal precondition with respect to Add(r) and Del(l) and must not be forgotten
at any nesting level in order to obtain the correct result. To that aim, we define
a partial shift construction which makes sure that the type graph of the main
body is never unselected in the µ-condition but is instead mapped in a consistent
way as a subgraph of the type graph of each variable. The following serves to
obtain the new type graphs containing the type of the main body:
Construction 1 (New type graphs for partial shift).
We assume that an arbitrary total order on all graph morphisms is fixed. If
c = b | µ[K]F is a µ-condition, then for a variable xi of K, XR,c (xi ) is defined
as the sequence of morphisms f obtained as below, in ascending order.
The morphisms f are obtained from P ′ by collecting all epimorphisms that
compose to monomorphisms with the pushout morphisms in the diagram:
∅ Pi
R X Pj′
f
Construction 2 (Partial shift).
Given monomorphisms x : G ֒→ H and y : R ֒→ H,
Px,y (b | µ[K]F) := Px,y (b) | µ[K ′ ]F ′ , where the new list of variables K ′ and
their respective types P ′ are obtained by concatenating all XR,c (xi ) of the vari-
ables of K in order. where the new variables and equations are obtained by
applying Pf,y to the variables of the left hand sides with all possible morphisms
f from R, as below, and accordingly to the right hand sides.
Px,y (xi ) = xyi if xi : G, where xyi : H is a new variable, H = cod(y).
a ι
Px,y (∃(P ֒→ C ′ ←֓ C, c′ )) is constructed as follows: Let Epi be the set of all
epimorphisms e with domain H ′ that compose to monomorphisms rW= e ◦ x′ and
b = e ◦ h with the pushout morphisms. Px,y (∃(P ֒→ C ′ ←֓ C, c′ ) = Epi ∃(H ֒→
E ←֓ J, Pi,y′ (c′ )): for each member of the disjunction, form the pullback of r ◦ ι
and b ◦ y, then pushout the obtained morphisms to (y ′ , i) as in the diagram:
B
ι
P C′ C c′
x x′ i
ι′
H h H′ J
y e
R y′ E
Boolean combinations of conditions are transformed to the corresponding com-
binations of the transformed members.
Remark 7 (Ambiguous Variable Contexts). Note that in a µ-condition it is
not necessarily true that in all contexts where xi is used, it appears with the
same morphism R ֒→ Pi (where R is the type of b). It is however possible to
equivalently transform every µ-condition into a “normal form” that has that
property. Applying PidR ,idR will by construction result in a µ-condition with
unambiguous inclusions R ֒→ Pi for all variables (namely the morphisms from
the sequences XR,c ), and this property is also preserved by the constructions
introduced later in this section. Unreachable variables created by X and P can
be pruned to obtain an equivalent, but sometimes smaller µ-condition.
Equivalence of conditions with placeholders (unlike µ-conditions) is only defined
for conditions using the same sets of variables, as equivalence in the sense of
nested conditions for each valuation. We extend A to conditions with placehold-
ers by defining Am (x) to be ∃(idcod(m) , m, x) if x : P .
One can show that Px,y is equivalent to Ax . The reason for introducing Px,y is
that it allows precise control over the types of the variables in the transformed
condition, which should include the type of the main body. Intuitively, as this
corresponds to the currently selected subgraph of a graph program, additions
and deletions are applied to that subgraph and one must make sure that the
changes apply to the whole µ-condition to obtain the correct result.
Lemma 1. The conditions Px,y (c) and Ax (c) are equivalent.
We introduce the transformations δ ′ m (c), α′ m (c) (based on auxiliary transfor-
mations δm,y (c) and αm,y (c), repsectively), which are used in the computation
of the weakest liberal precondition (with respect to addition and deletion, re-
spectively4 ), of a µ-condition that has already undergone partial shift:
Definition 10 (Transformations δ ′ and α′ ).
Let c : G be a condition with placeholders. If r : K ֒→ R and y : R ֒→ G (resp.
l : K ֒→ L and y : K ֒→ G) are monomorphisms, W thenWδr,y (c) (αl,y (c)) is defined
as follows: δr,y (¬c) = ¬δr,y (c)
W and δ r,y ( Wj∈J c j ) = j∈J δr,y (cj ) (respectively:
αl,y (¬c) = ¬αl,y (c) and αl,y ( j∈J cj ) = j∈J αl.y (cj )).
For c = ∃(a, ι, c′ ), the following constructions are used:
a′ ι′ δr,y′′ (c′ ) a′ ι′ δr,y′′ (c′ )
W X ′
V W X ′′V
′′ r ′′′ ′ l ′′′
h r r h l l
K P a C′ ι C c′ L P a C′ ι C c′
y y
r l
R y′ K y′
Case of δm,y (c′ ): If the pushout complement of r and a ◦ y does not exist, then
δm,y (c) = f alse. Otherwise, obtain it as x′ and r′ and pullback (a, r′ ) to (a′ , r′′ )
with source W ; this yields a morphism h from K to W to make the diagram
commute and the special PO-PB lemma [3] applicable. Pullback (ι, r′ ) to (ι′ , r′′′ ),
(x′ = a′ ◦ h) and let δm,y (c) = ∃(a′ , ι′ , δm,y′′ (c′ )) (the pullback property yields
existence and uniqueness of y ′′ between K and V to make it commute).
Case of αl,y (c): pushout (y, l) to (l′ , h); pushout (l′ , a) to (l′′ , a′ ); pullback (a′ ◦
h, l′′ ◦ι) and pushout to (y ′′ , l′′′ ) over the pullback (not drawn in the figure except
for the morphism l′′′′ ). The commuting morphism from the pushout object V to
X fills in to yield ∃(a′ , ι′ , αl,y (c′ )). The commuting morphism from L to V is y ′′ .
For variables, δm,y (xi ) = x′i is a new variable of type K, likewise αm (xi ) has type
L (see Rem. 7). Finally, δ ′ m (c) = δm,id (Pid,id (c)) and α′ m (c) = αm,id (Pid,id (c)).
In contrast to P, the transformations α′ and δ ′ leave the number of variables
unchanged. Only the types of the variables are modified. We recall that for any
l : K ֒→ L, there is a condition ∆(l) that expresses the possibility of effecting
Del(l), i.e. ∆(l) is satisfied exactly by the first components of tuples in JDel(l)K.
We describe ∆(l) only informally: f |= ∆(l) states the non-existence of edges
that are in im(f ) but incident to a node in im(f ) − im(f ◦ l).
Theorem 2 (Weakest Liberal Precondition for µ-conditions). For each
rule ̺, there is a transformation Wlp̺ that transforms µ-conditions to µ-condi-
tions and assigns to each condition c such that m′ |= c another condition Wlp̺ (c)
4
The letters were chosen so as to indicate the effect of the transformation: to compute
the weakest precondition with respect to addition, δ ′ needs to delete portions of the
morphisms in the condition, and vice versa.
with the property that m |= Wlp̺ (c) whenever (m′ , m, p) ∈ J̺K and Wlp̺ (c) is
the least condition with respect to implication having this property.
3.3 A Weakest Liberal Precondition Example
In this subsection, we construct a weakest liberal precondition of a µ-condition
step by step. Figure 2 shows a single-rule graph program which matches a node
with exactly one incoming and one outgoing edge and replaces this by a single
edge. The effect of the rule is to contract paths, and it can be applied as long as
no other edges are attached to the middle node.
3
Sel ∅ ֒→ ; Del ←֓ ; Add ֒→ ; U ns ←֓ ∅
1 2 1 2
Fig. 2. A path-contracting rule ̺contract = Selc ; Delc ; Addc ; U nsc .
Figure 3 shows a µ-condition whose weakest liberal precondition we wish to
compute. It is a typical example of a µ-condition, which evaluates to true on
those graphs that contain some node which has a path to every other node.
3
∃( , ∀( , x1)) where x1[ ] = ∃( ) ∨ ∃( , x1[ ])
1 1 2 1 2 1 2 1 2 1(3) 2(2)
Fig. 3. A µ-condition c3 = (b, l) expressing the existence of a node from which there
exists a path to every other node.
3
∃( ←֓ ∅, ∀( , x1)) where x1 [ ] = ∃( ) ∨ ∃( , x1 [ ])
1 2 1 2 1 2 1 2 1 2 1(3) 2(2)
Fig. 4. Wlp(U nsc , c3 ). Note that the nodes under the universal quantifier are not the
same as those of the outer existential quantifier, as these have been unselected: the
type of the subcondition ∀(...) is ∅.
In Figures 5 and 6, a partial shift has been applied to the condition of Fig-
ure 4 (Wlp(U nsc , c3 )), and the modifications the condition undergoes in the
computation of the weakest precondition with respect to Addc and Delc are
highlighted in various colours (see Figure 7 for a legend). Construction 1 has
yielded a new list of variables5 , x1 , ..., x7 , the corresponding equations are shown
in 6. Note that the representation is somewhat further abbreviated: type graphs
of variables are suppressed in the notation in subconditions ∃(a, ι, xi ), when the
mapping ι from the type graph to the target of a is the identity. No other sim-
plifications were applied. We have highlighted in yellow and red the type of the
main body of Wlp(U nsc , c3 ) throughout Figure 5; edges that are highlighted in
red are deleted to compute Wlp(Addc , Wlp(U nsc , c3 )) as per Def. 10; the edges
and nodes highlighted in red are not present initially, but added to compute
Wlp(Delc , Wlp(Addc , Wlp(U nsc , c3 ))) as per Def. 10, which is obtained by con-
joining ∆(l) to the main body (which we have not represented, as it is easy
to compute and would only encumber the illustration). In the end, a universal
5
Although the original µ-condition needed only one variable, the partial shift yields
a µ-condition with multiple variables in general.
3 4
3 3 3 3
∃ 1 2
,∀ 1 2
, x7 ∧ ∀ , x6 ∧ ∀ 1 2
, x4 ∧ ∀ 1 2
, x5 ∧ ∀ 1 2
, x3
1 2
5 5 5
5 5 5
∧∀ 1 2
, x1 ∧ ∀ 1 2
, x2
5 5
Fig. 5. Construction of Wlp(Delc ; Addc ; U nsc , ̺c ): main body (variables: see below).
h i 3 h 3(3) i
x1 1 2
=∃ ∨∃ 1 2
∨∃ 1 2
, x6
1 2 1(1) 2(2)
5 5
h i 35 h 3(3) 5 i 5(5)
x2 1 2
=∃ 1 2
∨∃ 1 2
, x5
1(1) 2(2)
5 5 5 5(5)
h3 i 3 3 h 2(3) 3(4) i 3(3) h 3(3) i
4
x3 1 2
=∃ 1 2
∨∃ 1 2
, x7 ∨∃ 1 2
, x4 ∨
1(1) 2(2) 1(1) 2(2)
5 5 5 5(5) 5 5(5)
3(3) h 3(3) i
∃ 1 2
, x4
1(1) 2(2)
5 5(5)
h3 i 3 3 h 3(4) 2(3) i 3(3) h 3(3) i
4
x4 1 2
=∃ 1 2
∨∃ 1 2
, x7 ∨∃ 1 2
, x3
1(1) 2(2) 1(1) 2(2)
5 5 5 5(5) 5 5(5)
h3 i 3 3 h 3(4) i 3 h i
4
x5 =∃ ∨∃ 1 2
, x5 ∨∃ 1 2
, x2
1 2 1 2 1(1) 2(2) 1(1) 2(2)
5 5 5 5(5) 5 5(5)
h3 i 3 3 h 3(4) i 3 h 1(1) 2(2) i
4
x6 1 2
=∃ 1 2
∨∃ 1 2
, x6 1 2
∨∃ 1 2
, x1
5 5 5 5 5 5(5)
h2 i 3 4 3 h 2(3) 3(5) i 3 h 3(4) i
3 4 5 4
x7 1 2
=∃ 1 2
∨∃ 1 2
, x7 ∨∃ 1 2
, x4 ∨
1(1) 2(2) 1(1) 2(2)
5 5 5 5(5) 5 5(5)
3 h 3(4) i
4
∃ 1 2
, x3
1(1) 2(2)
5 5(5)
Fig. 6. Construction of Wlp(Delc ; Addc ; U nsc , ̺c ): equations for the variables.
node/edge decoration meaning
items (nodes and edges) selected for W lp(U ns(y), c)
items to be deleted to obtain W lp(Add(r), c)
items to be added to obtain W lp(Del(l), c)
Fig. 7. Legend for Figure 5.
quantification with morphism ∅ ֒→ L completes the weakest precondition with
respect to the rule, as in the construction for nested conditions [12].
The outer existential quantifier in Fig. 5, where the unselection morphism is not
shown in the abbreviated representation, is really as in Fig. 8:
∃ ←֓ , ...
1 2 1 2
5 5
Fig. 8. Outer nesting level of the conditions in Fig. 5
When following the construction through the nesting levels, please keep in mind
that one may sometimes choose among isomorphic pushout objects and the
numbers of new nodes are arbitrary, but the nodes 1, 2 and (as created by
the transformation α′ ) 5 are never “unselected” and therefore present in every
type graph occurring in the weakest preconditions, similarly for the edges (not
numbered because their mapping is unambiguous in the example).
4 Correctness Relative to µ-conditions
In the previous section, we have shown how the weakest liberal precondition
construction for nested conditions carries over to µ-conditions. The next task is
to develop methods for deducing correctness relative to µ-conditions and extend
the proof calculus, for which we offer a partial solution in this section.
The soundness of Pennemann’s calculus K has been established in the publica-
tions introducing them, and recently a tableaux based completeness proof of K
was published [11]. The proof rules of K are easily seen to be sound for µ-condi-
tions as well, however the recursive definitions requires an extension.
For our calculus Kµ , we adopt the resolution-style rules of K and add an induc-
tion principle to deal with certain situations involving fixed points. This proved
to be sufficient to handle all the situations encountered in the examples.
We employ a sequent notation: the inference rules manipulate objects Ctx : Γ ⊢
∆, with the intended meaning that the disjunction of ∆ can be deduced from
the conjunction of Γ in the context Ctx. The context Ctx is a pair of a left
hand side of a sequent and an operator on µ-conditions. Γ and ∆ are sets of
expressions, which differ from conditions in that identifiers can be used for the
main bodies of µ-conditions and both these and variables can be annotated with
(n)
their recursion depth, an implicitly universally quantified natural number. xi
(n)
then stands for Fi (false) and an auxiliary rule permits to unroll it to the i-th
component of F applied to x(n−1) .
The induction rule announced above is (where Hi,j for each i ∈ {1, ..., kIk},
j ∈ {1, ..., kJk} is any condition with placeholders):
∀i,j
z }| {
(m) (n)
xi ∧ ¬yj ⊢ ⊢
(m−1) (n) (m−1) (n)
Hi,j (x1 ∧¬y1 , ..., xkIk ∧¬ykJk ) ∀i, j Hi,j (false) = false
W
xi ∧ ¬yi ⊢ false
(IndMuEmpty)
Theorem 3. Kµ := K ∪ {IndMuEmpty} is sound.
There are a number of details hidden in the discussion above: Boolean operations
must be lifted to µ-conditions, which entails variable renaming and union of the
systems of equations; rules for exploiting logical equivalences between different
Boolean combinations are necessary to equivalently transform conditions into a
form suitable for the application of the rules of K; in [12], each Boolean combi-
nation appearing inside a nested condition is put into conjunctive normal form
prior to the application of rules. Proof trees in the sequent-style calculus Kµ start
with instances of the axiom (A ⊢ A is derivable by a rule with no antecedents),
and make use of all the classical sequent rules [5] not involving quantifiers.
Our handling of nested contexts relies on substitutions: a context is a pair of a
left hand side of a sequent, and a graph condition with a special variable. The
rule for manipulating the context is usable both ways:
⊢ Ctx(x)
(Ctx)
Ctx ⊢ x
5 Related Work
Recently, Poskitt and Plump [16] have presented a weakest precondition calculus
for a different extension of nested conditions (monadic second-order conditions)
and demonstrated how to use it in a Hoare logic. The method is arguably closer
to reasoning directly in a logic and less graph condition like, but seems successful
at solving some of the same problems in a different way. HR∗ conditions [17] are
another approach towards the same goal; they have already been mentioned in
the main text and recently there has been an effort at extending the weakest
precondition calculus to a subclass including path expressions. Verification of
graph transformation system has also been performed within general-purpose
theorem proving environments by Strecker et al. [19, 13], with positive path
conditions. Verification of graph transformation systems via model checking of
abstractions, as opposed to the prover-based approach pursued here, can be
found in Gadducci et al., Baldan et al., König et al., Rensink et al. [4, 1, 10, 18].
A summary overview of graph conditions for non-local properties is attempted
below (a proof calculus is presented in [16] but completeness of a proof calculus
has only recently been obtained by Lambers and Orejas [11] for nested conditions
and remains to be researched for the other approaches). Note that while HR∗
conditions are known to properly contain the monadic second-order definable
properties [17] and nested conditions are a special case of each of the other
three, we have not yet been able to separate µ-conditions from MSO or HR∗ :
reference [12] (here) [17] [16]
conditions Nested µ- HR∗ MSO-
wlp yes yes incomplete6 yes
complete proof calculus yes future work
theorem prover yes future work
6
Radke, personal communication.
6 Conclusion and Outlook
We have introduced µ-conditions and achieved several results, mainly a weakest
liberal precondition transformation (Theorem 2), soundness of a proof calculus
(Theorem 3), and discussed correctness relative to µ-conditions, which appears
to be a fruitful ground for further investigations.
In analogy to the equivalence between first-order predicate graph logic and nested
graph conditions, we are investigating whether µ-conditions have the same ex-
pressivity as fixed point extensions to classical first-order logic for finite graphs.
Also, the expressivity of HR∗ conditions [17] or even MSO likely surpasses that
of µ-conditions, but the precise relationship remains to be examined. As the
examples show, the weakest precondition calculus (which is still a research ques-
tion for HR∗ conditions [17] but readily available by logical means in the MSO-
conditions formalism [16]) produces quite unwieldy expressions due to partial
shift. The blowup is exponential in the size of the interface graphs used in the
rule, and seems unavoidable because of the need to use a fixed set of type graphs
for the finitely many variables (and a blowup is also inherited from the weak-
est precondition calculus of [12]). Rule IndMuEmpty also contributes because
it involves a Cartesian product between variable sets. We have devised heuris-
tics to simplify the expressions, but even if many of the cases can be resolved
automatically, this issue still raises concerns as to the practical applicability.
Future work will also include tool support with special attention to semi-auto-
mated reasoning, based on the reasoning engine Enforce implemented in [12].
To extend the weakest liberal precondition construction to programs with it-
eration, one would have to provide, or have the prover attempt to determine,
an invariant, as in the original work of Pennemann; to obtain termination, one
could proceed as in [14] and prove a termination variant. We plan a further
generalisation to correctness under adverse conditions, i.e. systems subject to
environmental interference, also modelled as a graph program. Furthermore, it
appears that µ-conditions might readily generalise to temporal properties, even
with the option to nest temporal operators inside quantifiers, which would al-
low properties such as the preservation of a specific node to be expressed (but
require further proof rules). This could be achieved by introducing a temporal
next operator parameterised on atomic subprograms (the basic steps of Def. 4)
and since in the semantics of these program steps the relationship between the
interfaces is deterministic, this would again confer an unambiguous type to such
an expression and make it suitable for use as a subcondition. Whether this offers
any new insights remains to be seen. Eventually, we would also like to deal with
algebraic operations on attributes and extend our work to a practical verification
method that separates the graph specific concerns from other aspects and allows
proofs of properties that depend on both, for example involving data structures
whose elements should remain ordered. Finally, the limitations imposed by un-
decidability prompt the search for of restricted decidable classes.
Acknowledgements
We thank Annegret Habel, many other members of SCARE and the anonymous
reviewers for constructive criticism of the approach and the paper.
References
1. Baldan, P., König, B., König, B.: A logic for analyzing abstractions of graph trans-
formation systems. In: Static Analysis, pp. 255–272. Springer (2003)
2. Dijkstra, E.W.: A discipline of programming. Prentice Hall (1976)
3. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph
Transformation. Monographs in Theoretical Computer Science, Springer (2006)
4. Gadducci, F., Heckel, R., Koch, M.: A fully abstract model for graph-interpreted
temporal logic. In: TAGT’98. LNCS, vol. 1764, pp. 310–322 (1998)
5. Gentzen, G.: Untersuchungen über das logische Schließen. I. Mathematische
Zeitschrift 39(1), 176–210 (1935)
6. Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems
relative to nested conditions. Math. Struct. in Comp. Sci. 19(2), 245–296 (2009)
7. Habel, A., Pennemann, K.H., Rensink, A.: Weakest preconditions for high-level
programs. In: ICGT 2006. LNCS, vol. 4178, pp. 445–460 (2006)
8. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications
of the ACM 26(1), 53–56 (1983)
9. Kreutzer, S.: Pure and Applied Fixed-Point Logics. Ph.D. thesis, Dissertation the-
sis, RWTH Aachen (2002)
10. König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the
analysis of graph transformation systems. LNCS, vol. 3920, pp. 197–211 (2006)
11. Lambers, L., Orejas, F.: Tableau-based reasoning for graph properties. In: Graph
Transformation, LNCS, vol. 8571, pp. 17–32 (2014)
12. Pennemann, K.H.: Development of Correct Graph Transformation Systems. Ph.D.
thesis, Universität Oldenburg (2009)
13. Percebois, C., Strecker, M., Tran, H.N.: Rule-level verification of graph transfor-
mations for invariants based on edges’ transitive closure. In: SEFM 2013. LNCS,
vol. 8137, pp. 106–121 (2013)
14. Poskitt, C.M.: Verification of Graph Programs. Ph.D. thesis, University of York
(2013)
15. Poskitt, C.M., Plump, D.: Verifying total correctness of graph programs. Electronic
Communications of the EASST 61 (2013)
16. Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph pro-
grams. In: Graph Transformation, LNCS, vol. 8571, pp. 33–48 (2014)
17. Radke, H.: HR* graph conditions between counting monadic second-order and
second-order graph formulas. Electronic Communications of the EASST 61 (2013)
18. Rensink, A., Distefano, D.: Abstract graph transformation. ENTCS 157(1), 39–59
(2006)
19. Strecker, M.: Modeling and verifying graph transformations in proof assistants.
ENTCS 203(1), 135–148 (2008)
20. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J.
Math. 5(2), 285–309 (1955)