Attributed graph constraints

Abstract

Graph constraints were introduced in the area of graph transformation, in connection with the notion of (negative) application conditions, as a form to limit the applicability of transformation rules. However, in a previous paper, we showed that graph constraints may also play a significant role in the area of visual software modelling or in the specification and verification of semi-structured documents or websites (i.e. HTML or XML sets of documents). In that paper we present a sound and complete proof system for reasoning with this kind of constraints. Those results apply, in principle, to any category satisfying some given properties, but the category of (typed) attributed graphs does not satisfy these properties. In particular, the proof rules introduced for reasoning with standard graph constraints allow us to infer infinitary formulas, making the logic incomplete. In addition, using the straightforward generalization of standard graph constraints, there is no obvious way of stating properties about the attributes of the given graphs. In this paper we introduce a new formulation for attributed graph constraints. More precisely, the idea is to see these constraints as standard graph constraints whose attributes are just variables, together with a logic formula that expresses properties that must be satisfied by these attributes. Then a proof system, which extends the one introduced in the previous paper, is presented and it is shown to be sound and complete. © 2008 Springer-Verlag Berlin Heidelberg.