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 properties. 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.
graph program
The correctness proof is done in the style of Dijkstra’s [
In this section, we introduce graph conditions and graph programs. We assume
familiarity with graph transformation systems in the sense of Ehrig et al. [
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 ∅.
A brief review of nested conditions follows. Nested graph conditions were proposed by Habel and Pennemann. Finite nested conditions were later shown to be equally expressive as graph-interpreted first-order predicate logic. Graph conditions 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): – If J is a countable set and for all j ∈ J , cj is a condition (over P ), then
Wj∈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 of ∃(a, idcod(a), c). The usual abbreviations define the other standard operators: V is ¬ W ¬, ∀ 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 a condition c : P , denoted f |= c, iff c = true, c = ¬c′ and f 6|= c′, or c = Wj∈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′.
∃(P a f q G
C′
ι q ◦ ι
C, |= c′ ) 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 subcondition c′ which appears nested inside ∃(α, ι, c′).
Remark 1 (No Added Expressivity). Our conditions with ι are equally
expressive as the nested conditions defined in [
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 customarily 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 direction: 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”. |= ∃ show the morphisms’ node mappings. We also adopt the convention of not explicitly 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 approach with injective rules and injective matches. For technical reasons, we define graph transformations in terms of four elementary steps, namely selection, deletion, addition and unselection. Deletion and addition always apply to a selected 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
morphism records the changes effected by the program. Our programs are a proper
subset of those in Pennemann [
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 sequential (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 p′ = G1 ←l1֓ D1 ֒→r1 H1, p′′ = H1 ←l2֓ D2′ ֒→r2 H2 is defined as G l1←◦l֓2′ D′′ r2֒→◦r1′ H2 using the pullback (r1′, l2′) of (r1, l2). If P is a graph program, then so is its iteration P ∗; JP ∗K = Sj∈NJP 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 transl r formation, a rule ̺ = (L ←֓ K ֒→ R) being precisely simulated by the program Sel(∅ ֒→ L); Del(l); Add(r); U ns(∅ ֒→ R).
μ-Conditions
In this section, we define µ -conditions on the basis of nested graph conditions.
These are capable of expressing path and connectivity properties, which
frequently 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
correctness of some basic constructions. An example is provided at the end of this
section to illustrate the constructions step by step.
Nested conditions are a very successful approach to the specification of graph
properties for verification. However, they are unable to express non-local
properties such as connectedness. Our idea is to generalise nested conditions to
capture certain non-local properties by adding recursion. The resulting formalism
will be similar to first order fixed point logics, see e.g. Kreutzer [
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
ktuples 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.
By definition, V and W 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 [
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 equivalence. 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 conditions 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
nested 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[
) ∨ ∃( It is read as follows: the word “where” separates the main body from the equations. 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 syntactically 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 example 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.
Remark 5. The least fixed point of F is equivalent to Wn∈N F n(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.
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 precondition (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 [
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:
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: ∅ R
Pi X f
P ′ j 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 variables 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) = xiy if xi : G, where xi : H is a new variable, H = cod(y).
y Px,y(∃(P ֒→ C′ ←ι ֓ C, c′)) is constructed as follows: Let Epi be the set of all a epimorphisms e with domain H′ that compose to monomorphisms r = e ◦ x′ and b = e ◦ h with the pushout morphisms. Px,y(∃(P ֒→ C′ ←֓ C, c′) = WEpi ∃(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 x x′ ′ i H h H′ ι J y e R y′
E c′ Boolean combinations of conditions are transformed to the corresponding combinations 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 placeholders 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 transformations δ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, respectively4), 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, then δr,y(c) (αl,y(c)) is defined
as follows: δr,y(¬c) = ¬δr,y(c) and δr,y(Wj∈J cj ) = Wj∈J δr,y(cj ) (respectively:
αl,y(¬c) = ¬αl,y(c) and αl,y(Wj∈J cj ) = Wj∈J αl.y(cj )).
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 [
Theorem 2 (Weakest Liberal Precondition for µ -conditions). For each rule ̺, there is a transformation Wlp̺ that transforms µ -conditions to µ -conditions 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. l
K P a C′ ι C y
l′′′ y′ δr,y′′ (c′) c′ 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. 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
←֓
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
∃( 1 , ∀( 1 2 , x1)) where x1[
In Figures 5 and 6, a partial shift has been applied to the condition of
Figure 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
simplifications 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
conjoining Δ(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.
quantification with morphism ∅ ֒→ L completes the weakest precondition with
respect to the rule, as in the construction for nested conditions [
1 5 2 1 5 2
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
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
publications introducing them, and recently a tableaux based completeness proof of K
was published [
The induction rule announced above is (where Hi,j for each i ∈ {1, ..., kIk}, j ∈ {1, ..., kJ k} is any condition with placeholders): ∀i,j }| z (m) ∧ ¬y(jn) ⊢ { xi Hi,j(x(1m−1) ∧¬y(1n), ..., x(kmIk−1)∧¬y(knJ)k)
W xi ∧ ¬yi ⊢ false ⊢ ∀i, j Hi,j(false) = 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 [
Recently, Poskitt and Plump [
[
[
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
expressivity as fixed point extensions to classical first-order logic for finite graphs.
Also, the expressivity of HR∗ conditions [
We thank Annegret Habel, many other members of SCARE and the anonymous reviewers for constructive criticism of the approach and the paper.