Published in:
Mathematical Structures in Computer Science, 19 (2009) 2, Seite 245-296
Language:
English
DOI:
10.1017/s0960129508007202
ISSN:
0960-1295;
1469-8072
Origination:
Footnote:
Description:
<jats:p>In this paper we introduce the notions of nested constraints and application conditions, short nested conditions. For a category associated with a graphical representation such as graphs, conditions are a graphical and intuitive, yet precise, formalism that is well suited to describing structural properties. We show that nested graph conditions are expressively equivalent to first-order graph formulas. A part of the proof includes transformations between two satisfiability notions of conditions, namely<jats:private-char><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" mimetype="image" xlink:type="simple" xlink:href="S0960129508007202_char1" /></jats:private-char>-satisfiability and<jats:private-char><jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="gif" mimetype="image" xlink:type="simple" xlink:href="S0960129508007202_char2" /></jats:private-char>-satisfiability. We consider a number of transformations on conditions that can be composed to construct constraint-guaranteeing and constraint-preserving application conditions, weakest preconditions and strongest postconditions. The restriction of rule applications by conditions can be used to correct transformation systems by pruning transitions leading to states violating given constraints. Weakest preconditions and strongest postconditions can be used to verify the correctness of transformation systems with respect to pre- and postconditions.</jats:p>