We present a prototype for executing and verifying graph transformations. The transformations are written in a simple imperative programming language, and pre- and post-conditions as well as loop invariants are specified in the Description Logic ALC (whence the name of the tool). The programming language has a precisely defined operational semantics and a sound Hoare-style calculus. The tool consists of the following sub-components: a compiler to Java for executing the transformations; a verification condition generator; and a tableau prover for an extension of ALC capable of deciding the generated verification conditions. A description of these components and their interaction is the main purpose of this paper.
1 CNRS and Université de Grenoble
2 Université de Toulouse / IRIT
Provably correct transformations of graph structures become increasingly
important, for example for pointer manipulating programs, model driven engineering
(such as EMF [
Contributions: This paper presents a new language, called small-tALC, and
accompanying programming environment for executing graph transformations and
reasoning about them. Let us characterize in a few words what our work is about
and what it is not about:
– The primary aim of our development is to be able to reason about graph
transformations in a pre- / post-condition style: can we ensure that any
graph satisfying the pre-condition is transformed into a graph satisfying
the post-condition? Essential ingredients of such a setup are a language for
describing the transformations, and an assertional formalism for specifying
the pre- and post-conditions.
? Part of this research has been supported by the Climt project (ANR-11-BS02-016).
– The transformation language is an imperative programming language with
special operations for manipulating graphs. This language is endowed with
traditional control flow constructs (selection and loops) and elementary
statements for adding and deleting arcs of a graph. There is a select statement
that can be understood as a generalized, non-deterministic assignment
operation and whose purpose is to perform matchings of rules in a target graph.
After a high-level overview of small-tALC (Section 2), we will give a more
detailed account of the program logic (in Section 3.1) and transformation
language (in Section 3.2). Our transformation language is by no means a
full-fledged programming language: for example, arithmetic operations are
excluded.
– The transformation language is not graphical, but textual. We do not
question the utility and appeal of a graphical notation, but this issue is orthogonal
to our concerns. We can imagine to couple small-tALC with existing graphical
editors, such as Henshin [
Altogether, we are thus primarily interested in proofs of correctness of graph transformations, for which two major approaches have emerged: 1. Model checking of graph transformations: given an initial graph and a set of transformation rules, check whether the graph can eventually evolve into a graph having certain properties, or whether specific properties can be ascertained to be always satisfied. This kind of reasoning is possible in principle (the initial graph can be specified by a pre-condition, invariants can be specified as loop conditions, eventuality properties as post-conditions), but our approach is clearly not geared towards this activity. 2. Full correctness proofs: given an arbitrary graph satisfying the pre-condition, verify that it evolves into a graph satisfying the post-condition. This is the kind of verification we are aiming at.
Full correctness proofs are hard, and undecidability of the generated proof
obligations is a major concern for rich logics [
The work described here has reached the state of a sound prototype. In the corresponding sections, we will make precise which parts of the development are completed to which degree, and indicate which missing parts still have to be filled in. The small-tALC environment is available from the following web page, where it will be regularly updated: http://www.irit.fr/~Martin.Strecker/ CLIMT/Software/smalltalc.html.
Related work: Hoare-like logics have already been used to reason on graph
transformations (see, e.g. [
Other tools dedicated to reasoning on graph transformations have been
proposed. For example, the GROOVE [
The computation of weakest preconditions from a graph rewriting system
is described by Habel, Pennemann and Rensink [
In a similar vein, Asztalos et al. [
Raven3 is a tool suite designed to handle and manipulate graph automata. In some sense Raven tends to generalize model-checking techniques from word to graph processing. Therefore techniques behind Raven tool are not directly comparable to small-tALC.
Alloy [
To explore the perspective of a user of small-tALC, we will walk through
processing a simple program, but before, let us take a look at the kind of graphs
we will be transforming, such as the example graph in Figure 1a (displayed with
RDF-Gravity4). We will be processing graphs in RDF [
Let us now turn to transformation programs, as the one depicted in Figure 2. A program is composed of one or several parameterized rules; and a parameterless main rule whose purpose is to specify the input- and output graph to be transformed and to identify the root nodes of the input graph. Rules can be assimilated to non-recursive procedures or macros. Procedural abstraction is so far not fully developed in our framework, so the analysis presented in the following concentrates on rule bodies.
The rule ex_rule has a precondition (pre) saying that node a is only connected (via arcs of type r) to nodes of type A, and that b is only connected to 4 http://semweb.salzburgresearch.at/apps/rdf-gravity/ concepts A, B; roles r; rule ex_rule (a, b) { vars c; pre: (a : ([!] r A)) && (b : ([!] r B)); select c with (b r c); add (a r c); post: (a : ([?] r B)); } rule main () { vars a, b; ingraph "input_graph.rdf"; outgraph "output_graph.rdf"; a := node("a0"); b := node("b0"); ex_rule(a, b); } nodes of type B. The program now does the following: among the nodes that b is connected to, we non-deterministically pick a node c and introduce an arc r between a and c. For example, the program might introduce an arc between a0 and b1 in the graph of Figure 1a (or between a0 and b2). We can now assert that after running this program, the node that variable a points to is connected via r to at least one element of type B, as expressed in the postcondition.
Suppose the example program is in file example.trans. Running the verifier as follows confirms that the program is correct, i.e. that any graph satisfying the precondition is transformed into a graph satisfying the postcondition. > graphprover example starting proof ...formula valid
Let us modify the post-condition, claiming that a is exclusively connected to elements of type B: post: (a : ([!] r B));
When running the verifier again, we see that the property is incorrect, and that a counter-model has been created (see Figure 1b, here displayed with Graphviz5). This counter-model describes the state at the beginning of the program, namely a graph with four nodes, where c1 is of type A and not of type B, and c2 of type B. Clearly, when connecting a with c2, the post-condition is violated.
We correct the post-condition, saying that a is only connected to elements of type A or B: post: (a : ([!] r (A [||] B))); Running the verifier again convinces us that this property is satisfied.
How does the verifier validate or invalidate a program? The approach is classic: from the annotated program, we extract a proof obligation by computing weakest pre-conditions (see Section 3.2). This is an ALC formula that is sent to a tableau decision procedure (described in Section 5.2). A failed proof attempt produces a saturated tableau from which a counter-model can always be extracted.
Operational semantics
Program logic
Decision procedure Code Extraction (Scala/Java)
Program prover (verified)
Eclipse
environment
(unverified)
Major parts of small-tALC have a strong formal basis and are being developed in
a proof assistant. We use Isabelle [
Our logic is a three-tier framework, the first level being Description Logic (DL) concepts, the second level facts, the third level formulas (Boolean combinations of facts and a simple form of quantification). Formulas occur not only in assertions (such as pre- and postconditions), but also in statements (Boolean conditions and select statement).
Concepts: In this paper, we concentrate on the description logic ALC [
C ::= ? (empty concept) j a (atomic concept) j : C (complement) j C u C (intersection) j C t C (union) j ([?] r C) (some) j ([!] r C) (all) j C (explicit substitution)
The semantics of DLs is given by Kripke structures or, differently speaking, by typed graphs. Under this interpretation, concepts represent sets of individuals. The constructors :; u; t (in Ascii notation: !,[&&],[||]) then have the obvious meaning. ([?] r C) is the set of individuals x such that there is at least one rtyped edge (x r y) between x and y, where y belongs to C. Dually, ([!] r C) is the set of individuals x all of whose r-edges go to individuals of type C.
The last constructor, explicit substitution [
Facts: Facts make assertions about an instance being an element of a concept, and about being in a relation. The grammar of facts is defined as follows: f act ::= i : C (instance of concept) j i r i (instance of role) j i (:r) i (instance of role complement) j i i (equality of instances) j i 6 i (inequality of instances)
Please note that since concepts are closed by complement, facts are closed by negation (the negation of a fact is again representable as a fact), and this is the main motivation for introducing the constructors “instance of role complement” and “inequality of instances”.
Formulas: A formula is a Boolean combination of facts. We also allow quantification over individuals i (but not over relations or concepts), and, again, have a constructor for explicit substitution. We overload the notation ? for empty concepts and the Falsum.
f orm ::= ? j f act j :f orm j f orm ^ f orm j f orm _ f orm j 8i:f orm j 9i:f orm j f orm
In Figure 2, we use the Ascii notation !, &&, || for negation, conjunction and disjunction. The extension of interpretations from facts to formulas is standard. As usual, a formula that is true under all interpretations is called valid.
When calculating weakest preconditions (in Section 5.1), we obtain formulas which essentially contain no existential quantifiers; we keep them as constructor because they can occur as intermediate result of computations. We say that a formula is essentially universally quantified if 8 only occurs below an even and 9 only below an odd number of negations. For example, :(9x: x : C ^ :(8y: y : D)) is essentially universally quantified. 3.2
Programming Language The programming language is an imperative language manipulating relational structures. Its distinctive features are conditions (in conditional statements and loops) that are restricted formulas of the logic ALC, in the sense of Section 3.1. It has a non-deterministic assignment statement select ... with allowing to select an element satisfying a fact. Traditional types (numbers, arrays, inductive types) and accompanying operations are not provided; the language is thus only targeted at transformations of graphs.
Statements of our language are defined by the following grammar: stmt ::= Skip (empty statement) j select i with f orm (assignment) j delete(i : C) (delete element from concept) j add(i : C) (add element to concept) j delete(i r i) (delete edge from relation) j add(i r i) (insert edge in relation) j stmt ; stmt (sequence) j if f orm then stmt else stmt j while f orm do stmt
Please note that the keywords add and delete are overloaded for nodes and for edges. There is no direct support for creating or deleting nodes in a graph, only for “moving” them between concepts. We intend to simulate node creation and deletion by providing a predefined concept heap such that add(n: heap) corresponds to creating node n and delete(n: heap) to deallocating node n. Details still have to be worked out.
The semantics is a big-step semantics with rules of the form (st; ) ) 0 expressing that executing statement st in state produces a new state 0.
The rules of the semantics are given in the Figure 4. Beware that we overload logical symbols such as 9, ^ and : for use in the meta-syntax and as constructors of f orm.
We do not enter into the details (also see the Isabelle formalization). Intuitively, the states manipulated by the operational semantics are the same as the interpretations of formulas, and they describe the current structure of a graph: which nodes are contained in each concept; which pair of nodes are contained in a role; and which variables are bound to which nodes. We write (b) to evaluate the condition b (a formula) in state .
Most of the rules are standard, apart from the fact that we do not use expressions, but formulas as conditions. The auxiliary function delete_edge modifies the state by removing an r-edge between the elements represented by v1 and v2, and similarly for generate_edge. There are analogous functions for adding / deleting in concepts.
(EDel) (Skip)
(Skip; ) ) 0 = delete_edge v1 r v2 (delete(v1 r v2); ) ) 0 (Seq) (c1; ) ) (c1;c2; ) ) (if b then c1 else c2; ) ) 0 (IfF) : (b) (c2; ) )
0 (if b then c1 else c2; ) ) 0 (WT) (b) (c; ) ) (while b do c; ) ) 00 (while b do c; 00) ) 0 0 (WF)
: (b) (while b do c; ) )
The statement select v with F (v) selects an element vi that satisfies formula F , and assigns it to v. For example, select a with a : A ^ (a r b) selects an element a which is and instance of concept A and being r-related with a given element b.
select is a generalization of a traditional assignment statement. There may be several instances that satisfy F , and the expressiveness of the logic might not suffice to distinguish them. In this case, any such element is selected, nondeterministically. Let us spell out the precondition of (SelAssT): Here, [v:=vi] is an interpretation update for individuals, modifying for variable v and assigning it a value vi in the semantic domain. We check whether the formula b would be satisfied under this choice, and if it is the case, keep this assignment. In case no satisfying instance exists, the semantics blocks, i.e. the given state does not have a successor state, which can be considered as an error situation. 4
Generating Java Code: For processing small-tALC programs such as the one in Figure 2 and generating Java code, we use the Eclipse environment and, in particular, the Xtext6 facilities for parsing, syntax highlighting and context-dependent help. The program prover is currently not fully integrated in this framework, so
that the interaction with the prover is performed via shell commands as described in Section 2.1.
In order to generate Java code for small-tALC programs, we parse the program and then traverse the syntax tree with Xtext/Xtend, issuing calls to appropriate Java functions that manipulate a graph (which is initially the input graph provided in the program’s main rule). Here is a glimpse at the Xtend code snippet that translates statements, in particular the add statement for roles: def statement(Stmt s){ switch s{
Add_stmt: add(s.lvar,s.role,s.rvar) ...
} } def add(String lvar,String role,String rvar)’’’
«graph».insertEdge(«lvar»,«role»,«rvar»);’’’
Thus, a small-tALC program fragment add(a r b); is translated to a Java
call g.insertEdge(a, r, b);, where the graph g is the current graph.
Transforming Graphs: Once a Java program has been generated for a given
small-tALC program, it can be compiled and linked with a library that provides
graph manipulating functions such as the above-mentioned insertEdge. When
executing this program, it remains to read an input file containing a graph
description, to perform the transformation and to output the new graph. We
represent graphs in the RDF [
For proving program correctness, we use a standard approach in program verification. For proving that a program prog establishes the postcondition Q if started in a state satisfying the precondition P , we calculate the weakest precondition of prog with respect to Q and then show that P implies this weakest precondition.
The details are inspired by the description in [
Without going further into program semantics issues, let us only state the following soundness result that relates the operational semantics and the functions wp and vc: Theorem 1 (Soundness). If vc(c; Q) is valid and (c; ) ) implies 0(Q). 0, then (wp(c; Q))
What is more relevant for our purposes is the structure of the formulas generated by wp and vc, because it has an impact on the decision procedure for the DL fragment under consideration here. Besides the notion of “essentially universally quantified” introduced in Section 3.1, we need the notion of quantifier-free formula: A formula not containing a quantifier. In extension, we say that a statement is quantifier-free if all of its formulas are quantifier-free.
By induction on c, one shows: Lemma 1 (Universally quantified). Let Q be essentially universally quantified and c be a quantifier-free statement. Then wp(c; Q) and vc(c; Q) are essentially universally quantified.
There is one major problem with the definition of function wp: the substitutions, such as C := C fvg or r := r (v1; v2). When conceiving them as a meta-operations, as is usually done, we see that substitutions would yield syntactically ill-formed formulas. For example, reducing ([?] r C)[C := C fvg] would give ([?] r (C fvg)), which is not a valid concept expression. There are two ways out of this difficulty: we could either relax our syntax and accept expressions of the form ([?] r (C fvg)). This would induce a rather heavy change on the logic. Alternatively, we can treat substitution as a constructor of our language. This is the approach we have adopted, and therefore, substitutions appear as syntactic elements in the definitions of Section 3.1. It remains to be seen (in Section 5.2) how substitutions can be dealt with by proof methods of ALC. 5.2
Tableau Method
The core of the decision procedure for proving the verification conditions that
are obtained as described in Section 5.1 is a tableau calculus which combines
the traditional logical rules of a tableau calculus [
As a consequence, and departing again from common practice in the DL literature, our tableau procedure does not manipulate facts (in the sense of Section 3.1), but formulas, i.e. Boolean combinations of facts. This extension becomes necessary because elimination of substitutions generates complex formulas. These could in principle be directly decomposed into sub-tableaux, but such a procedure obscures both the presentation and the implementation. Preprocessing: The tableau manipulates quantifier-free formulas in negation normal form (nnf ).
The formulas obtained from function vc do possibly contain quantifiers, but as mentioned before, the formulas are essentially universally quantified. To get rid of these quantifiers, we therefore perform the following steps: – We convert the entry formula f to a prenex normal form, i.e. a form 8x1 : : : xn:b with quantifier-free body b. – We drop the quantifier prefix; more precisely, we replace the bound variables x1 : : : xn in b by free variables. This transformation preserves validity. – We start the tableau with nnf (:b). The procedure is a satisfiability check that either produces an empty tableau (meaning that f is valid) or a model of :b that is a counter-example of f .
In negation normal form, negations only occur in front of atomic concepts (of the form :a, where a is an atomic concept). This invariant is maintained throughout the tableau procedure. 5.3
Tableau Rules In the following, we present a high-level description of the tableau procedure. (The reader consulting the Isabelle theories will notice that the formalization is on two levels: a set-based, relational version, aiming at proving essential properties such as soundness and completeness of the rules; and a list-based implementation. The formal proofs of these theories are not yet finalized.)
A tableau manipulates sets of branches (also called abox es - “assertional boxes” in DL terminology). Each branch is a set of formulas. We first concentrate on a set of rules aiming at decomposing formulas on a single branch. They have the form ,! 0, expressing that branch is rewriten to 0. We write ; f instead of [ ff g for adding formula f to . The rules are displayed in Figure 6.
Let us comment on the rules: The structural rules conjC, disjCr, disjCl (for concepts) and conjF, disjFr, disjFl (for formulas) should be clear. The rule all allows to conclude y : C if x is only r-connected to elements of type C, and there is an arc (x r y). The rule some inserts an arc (x r z) and a membership z : C for an arbitrary z if it is known that x is r-connected to at least one element of type C. The rule eq propagates an equality x y in the branch, provided the equality is not x x.
conjC (x : (C1 u C2)) 2 not((x : C1) 2 and (x : C2) 2
) ,! ; (x : C1); (x : C2) disjCr disjCl all (x : (C1 t C2)) 2 (x : (C1 t C2)) 2 (x : ([!] r C)) 2
(x : C1) 2= ,! ; (x : C1)
(x : C1) 2= ,! ; (x : C2) (x r y) 2 ,! ; (y : C) (x : C2) 2= (x : C2) 2= (y : C) 2= some (x : ([?] r C)) 2 for all y; not((x r y) 2 ,! ; (x r z); (z : C) and (y : C) 2 ) subst (x : (C )) 2 ,! ; nnf (push((x : C) ))
nnf (push((x : C) )) 2= eq (x y) 2 ,!
x 6= y [x := y] conjF f1 ^ f2 2 not(f1 2 and f2 2
) ,! ; f1; f2 disjFr f1 _ f2 2
f1 2= ,! ; f1 f2 2= disjFl f1 _ f2 2
f1 2= ,! ; f2 f2 2=
The rule subst is applicable for concepts with substitutions. As motivated in Section 5.1, substitutions cannot be eliminated at once, but they can be removed progressively, whenever the tableau prover hits on a fact of the form (x : C ). Note that the variable x was possibly not present in the original tableau with which we have started the proof, but may have been introduced by a some-rule. If we encounter such a situation, we push the substitution as far as possible. We postpone the details to Section 5.5.
A branch contains a clash (clash( )) if either of the following holds: – for x a variable, (x : ?) 2 – for x a variable and a an atomic concept, (x : a) 2 – for x; y variables, (x r y) 2 and (x (:r) y) 2 and (x : :a) 2 – for x a variable, (x 6 x) 2 – ? 2
Tableau Procedure We can now formulate a depth-first-search function df s exploring a tableau. The function takes a tableau (here implemented as a list of branches) and returns a list of models. Initially, the tableau is just the formula [ff g] to be proved. If the resulting list is empty, f is not satisfiable. Otherwise, the list contains an element which is a model of f .
df s[ ] = [ ] df s( :: s) = if clash( ) then df s( s) else if reducible( ) then df s(f 0j ,! else [ ]
The procedure progressively eliminates all inconsistent branches (with clash( )). If a branch is not inconsistent, but reducible (i.e. , there exists a 0 with ,! 0), then we expand the tableau and explore the new branches. 5.5
Eliminating Substitutions The push function used in the subst rule of Figure 6 pushes substitutions into formulas, “as far as possible”. The remaining tableau rules then decompose formulas until substitutions hidden in subformulas become apparent and the subst rule can be applied again. Intuitively speaking, this process decreases the “height” of the substitutions in a formula, until they eventually disappear.
For a formula f , we define push(f ) as the formula f 0 which is the result of the rewrite system spelled out in the following. Thus: push(f ) = f 0 iff f f 0, where the rewrite relation is defined in the following. There are numerous cases to consider, and we do not present all of them.
Substitution in formulas are pushed into subformulas: – ? ? – (:f ) – (f1 ^ f2) – (f1 _ f2) (:f ) (f1 ^ f2 ) (f1 _ f2 ) – (x : :C) – (x : C1 u C2) – (x : C1 t C2) Substitution in facts: Substitutions of individual variables f [x := y] are carried out as expected. Otherwise, we procede as follows: – For substitutions of the form a := a fvg or a := a + fvg: (x : c)[a := a fvg] (x : c) for a 6= c, and similarly for a := a + fvg (x : a)[a := a fvg] (x : a) ^ x 6= v (x : a)[a := a + fvg] (x : a) _ x = v (x : ([?] r C))[a := a fvg] (x : ([?] r C[a := a fvg])), and similarly for the other combinations involving constructor [?] or [!] and substitutions a := a + = fvg. – For substitutions of the form r := r f(v1; v2)g or r := r + f(v1; v2)g: (x : c)[r := r f(v1; v2)g] x : c, and similarly for r + f(v1; v2)g (x : ([!] r0 C))[r := r f(v1; v2)g] (x : ([!] r0 C)) for r 6= r0 (x : ([!] r C))[r := r f(v1; v2)g] ite ((x = v1) ^ (v2 : (:C[r := r (v1; v2)])) ^ (v1 r v2); (x : (< 2 r (:C[r := r (v1; v2)]))); (x : ([!] r C[r := r (v1; v2)]))) Here, ite is for if-then-else: ite(a; b; c) = (a ! b) ^ (:a ! c).
Please note that the logic ALC cannot completely express the effect of substitution, and we have to resort to the more expressive logic ALCQ, which turns out to be complete for substitutions. Thus, the “then” branch of the ite construct expresses that x is r-connected to less than 2 elements of (:C[r := r (v1; v2)]). We have however not yet implemented tableau rules for ALCQ, so we stick to the simpler logic in this presentation. (x : ([!] r C))[r := r + f(v1; v2)] :((x = v1) ^ (v2 : :(C[r := r + (v1; v2)])) ^ (v1 (:r) v2)) ^(x : ([!] r (C[r := r + (v1; v2)])))
Similar rules for existential quantification (x : ([?] r C)). 6
We have presented small-tALC, a framework for executing graph transformations and proving their correctness with a sound and complete calculus. One of the distinctive features of the approach is its formal semantic basis. We are now moving towards application, such as Sparql Query and Update in the knowledge representation world, and model transformations as used in model-driven engineering. The greatest challenge is the development of logics that are more expressive than ALC but remain decidable. Even though a low proof-theoretic complexity is not a major concern for program correctness proofs (these are not executed on a large knowledge base), the concern changes when wanting to execute programs efficiently on a large data set.
Acknowledgements We are grateful to María Espinoza who has helped us
explore the applicability of graph transformations to the RDF world [