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 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 abstractions, 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, Pennemann 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: The correctness proof is done in the style of Dijkstra's [2] predicate transformer 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].
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.
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 conditions 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 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, c j is a condition (over P ), then j∈J c j 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 Cond P is the class of all conditions over P . We may write ∃(a, c) instead of ∃(a, id cod(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.
A monomorphism f : P ֒→ G satisfies a condition 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 [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
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 show the morphisms' node mappings. We also adopt the convention of not explicitly representing the morphism ι in a situation ∃(a, ι, x i ); 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 [12], and use the same semantics.
Definition 4 (Graph Programs).
In the following table, x, l, r, y, m in and m out are monomorphisms, with x, l, r and y arbitrarily chosen to define a program step, while m in and m out are called interfaces and universally quantified in the set comprehensions that appear in the definitions below.
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 P ∪ Q and the semantics of sequence is
. If P is a graph program, then so is its iteration P * ; P * = j∈N P j where P j = P ; P j−1 for j ≥ 1 and P 0 = skip. 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 [9]. The reader might want to compare our µ-conditions to a distinct formalism towards expressing 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 nonlocal properties, such as MSO-conditions [16] because µ-conditions provide a new and different generalisation of nested conditions, and neither is it immediately 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 P . Indexed typewriter letters x 1 stand for placeholders, i.e. variables. The notation c : P indicating that c has type P is also extended to sequences: c : P (provided c = P ).
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 Cond P , one can define monotonic operators on Cond P . 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 .
To represent systems of simultaneous equations, we work on tuples of conditions. If P = P 1 , . . . , P P is a sequence of graphs, then Cond P is the set of all Ptuples c of conditions, whose i-th element is a condition over the i-th graph of P . Satisfaction is defined component-wise:
By definition, and of countable sets of Cond P 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 Cond P 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 from P over P is a (graph) condition with placeholders is either ∃(a, ι, c), or ¬c, or j∈J c j , or x i , 1 ≤ i ≤ P where x i is a variable of type P i .
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 ∈ Cond P , then F[x/c] is obtained by substituting each occurrence of x i by c i for all i ∈ {1, ..., P }.
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 ∈ Cond P ). 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 {F i } i∈{1,..., P } are conditions with placeholders from P , over the graphs of P respectively, then µ[P ]F denotes the least fixed point of the operator c → F [x/c].
A µ-condition is a pair (b, l) consisting of a condition with placeholders b, and a finite list of pairs l = (x i , F i (x)) of a variable x i : P i and a condition F i (x) : P i , with placeholders from x, for some graph P i , such that F is monotonic.
Notation. we write the list of pairs l = (x i , F i (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 Cond P .
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.
] where x 1 [
) ∨ ∃(
])
It is read as follows: the word "where" separates the main body from the equations. Here, x 1 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 x 1 , 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 F i (x) is equivalent to a nested condition.
The following fact is well-known: 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:
Theorem 1 (Deciding Satisfaction of µ-conditions). Given a morphism f : P ֒→ G and a µ-condition c, it is decidable whether f |= c.
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
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 A m (c) from [12] whose fundamental property is to transform any nested condition c into another nested condition such that m ′′ |= A m (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 ′ ) that compose to monomorphisms b := e • a ′ and r
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.
) 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:
Given monomorphisms x : G ֒→ H and y : R ֒→ H,
where the new list of variables K ′ and their respective types P ′ are obtained by concatenating all X R,c (x i ) of the variables of K in order. where the new variables and equations are obtained by applying P f,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.
) is constructed as follows: Let Epi be the set of all epimorphisms e with domain H ′ that compose to monomorphisms r = e • x ′ and b = e • h with the pushout morphisms. P x,y (∃(P ֒→ C ′ ←֓ C, c ′ ) = Epi ∃(H ֒→ E ←֓ J, P i,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:
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 x i is used, it appears with the same morphism R ֒→ P i (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 P id R ,id R will by construction result in a µ-condition with unambiguous inclusions R ֒→ P i for all variables (namely the morphisms from the sequences X R,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 A m (x) to be ∃(id cod(m) , m, x) if x : P .
One can show that P x,y is equivalent to A x . The reason for introducing P x,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 P x,y (c) and A x (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, respectively 4 ), 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 ( j∈J c j ) = j∈J δ r,y (c j ) (respectively: α l,y (¬c) = ¬α l,y (c) and α l,y ( j∈J c j ) = j∈J α l.y (c j )).
For c = ∃(a, ι, c ′ ), the following constructions are used:
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 (x i ) = x ′ i is a new variable of type K, likewise α m (x i ) has type L (see Rem. 7). Finally, δ ′ m (c) = δ m,id (P id,id (c)) and α ′ m (c) = α m,id (P id,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 Del(l) . 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
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)
with the property that m |= Wlp ̺ (c) whenever (m ′ , m, p) ∈ ̺ 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.
; Add ֒→ ; U ns ←֓ ∅ 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.
∃(
, x 1 )) where x 1 [
) ∨ ∃(
])
Fig. 3. A µ-condition c3 = (b, l) expressing the existence of a node from which there exists a path to every other node.
∃(
, x 1 )) where x 1 [
) ∨ ∃(
])
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 Figure 4 (Wlp(U ns c , c 3 )), and the modifications the condition undergoes in the computation of the weakest precondition with respect to Add c and Del c are highlighted in various colours (see Figure 7 for a legend). Construction 1 has yielded a new list of variables5 , x 1 , ..., x 7 , 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, ι, x i ), 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 ns c , c 3 ) throughout Figure 5; edges that are highlighted in red are deleted to compute Wlp(Add c , Wlp(U ns c , c 3 )) as per Def. 10; the edges and nodes highlighted in red are not present initially, but added to compute Wlp(Del c , Wlp(Add c , Wlp(U ns c , c 3 ))) 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
, x 2 Fig. 5. Construction of Wlp(Delc; Addc; U nsc, ̺c): main body (variables: see below).
x
x
∨ ∃
∨ ∃
x 4 1 2
∨ ∃
x 5
∨ ∃
x 6 1 2 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) 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:
, ... 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).
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 [11]. The proof rules of K are easily seen to be sound for µ-conditions as well, however the recursive definitions requires an extension.
For our calculus K µ , we adopt the resolution-style rules of K and add an induction 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 their recursion depth, an implicitly universally quantified natural number. x (n) i then stands for F (n) i (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 H i,j for each i ∈ {1, ..., I }, j ∈ {1, ..., J } is any condition with placeholders):
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 combination 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:
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 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]
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 [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 question for HR * conditions [17] but readily available by logical means in the MSOconditions 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 weakest precondition calculus of [12]). Rule IndMuEmpty also contributes because it involves a Cartesian product between variable sets. We have devised heuristics 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-automated reasoning, based on the reasoning engine Enforce implemented in [12].
To extend the weakest liberal precondition construction to programs with iteration, 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 allow 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 undecidability prompt the search for of restricted decidable classes.
We thank Annegret Habel, many other members of SCARE and the anonymous reviewers for constructive criticism of the approach and the paper.
⋆ This work is supported by the German Research Foundation (DFG), grant GRK 1765 (Research Training Group -System Correctness under Adverse Conditions)