{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T16:23:56Z","timestamp":1791217436098,"version":"4.1.0"},"reference-count":35,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T00:00:00Z","timestamp":1238544000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2009,4]]},"abstract":"<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>","DOI":"10.1017\/s0960129508007202","type":"journal-article","created":{"date-parts":[[2009,1,13]],"date-time":"2009-01-13T10:26:44Z","timestamp":1231842404000},"page":"245-296","source":"Crossref","is-referenced-by-count":153,"title":["Correctness of high-level transformation systems relative to nested conditions"],"prefix":"10.1017","volume":"19","author":[{"given":"ANNEGRET","family":"HABEL","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KARL-HEINZ","family":"PENNEMANN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2009,4,1]]},"reference":[{"key":"S0960129508007202_ref4","doi-asserted-by":"publisher","DOI":"10.1142\/9789812384720_0003"},{"key":"S0960129508007202_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025714"},{"key":"S0960129508007202_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45832-8_18"},{"key":"S0960129508007202_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30203-2_23"},{"key":"S0960129508007202_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80188-4"},{"key":"S0960129508007202_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11841883_30"},{"key":"S0960129508007202_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.075"},{"key":"S0960129508007202_ref10","first-page":"135","article-title":"Theory of constraints and application conditions: From graphs to high-level structures","volume":"74","author":"Ehrig","year":"2006","journal-title":"Fundamenta Informaticae"},{"key":"S0960129508007202_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003425"},{"key":"S0960129508007202_ref17","doi-asserted-by":"crossref","first-page":"287","DOI":"10.3233\/FI-1996-263404","article-title":"Graph grammars with negative application conditions","volume":"26","author":"Habel","year":"1996","journal-title":"Fundamenta Informaticae"},{"key":"S0960129508007202_ref34","unstructured":"Zuckschwerdt C. (2006) Ein System zur Transformation von Konsistenz in Anwendungsbedingungen (in German). Berichte aus dem Department f\u00fcr Informatik, Universit\u00e4t Oldenburg 11\/06, 114 pages."},{"key":"S0960129508007202_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-95486-3_7"},{"key":"S0960129508007202_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2004.11.002"},{"key":"S0960129508007202_ref2","doi-asserted-by":"crossref","unstructured":"Azab K. and Habel A. (2008) High-level programs and program conditions. In: Graph Transformations (ICGT 2008). To appear in Springer-Verlag Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-540-87405-8_15"},{"key":"S0960129508007202_ref1","volume-title":"Abstract and Concrete Categories","author":"Ad\u00e1mek","year":"1990"},{"key":"S0960129508007202_ref5","first-page":"193","volume-title":"Handbook of Theoretical Computer Science","author":"Courcelle","year":"1990"},{"key":"S0960129508007202_ref6","doi-asserted-by":"publisher","DOI":"10.1142\/9789812384720_0005"},{"key":"S0960129508007202_ref7","volume-title":"A Discipline of Programming","author":"Dijkstra","year":"1975"},{"key":"S0960129508007202_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31847-7_17"},{"key":"S0960129508007202_ref8","volume-title":"Predicate Calculus and Program Semantics","author":"Dijkstra","year":"1989"},{"key":"S0960129508007202_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30203-2_11"},{"key":"S0960129508007202_ref11","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"Ehrig","year":"2006"},{"key":"S0960129508007202_ref15","doi-asserted-by":"publisher","DOI":"10.1142\/9789812384720_0004"},{"key":"#cr-split#-S0960129508007202_ref16.1","unstructured":"3. European Telecommunications Standards Institute (1998) Digital cellular telecommunications system (Phase 2+)"},{"key":"#cr-split#-S0960129508007202_ref16.2","unstructured":"4. Handover procedures. Technical Specification, ETSI TS 100 527 V7.0.0 1999-08 (GSM 03.09 version 7.0.0 Release 1998)."},{"key":"S0960129508007202_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/11841883_31"},{"key":"S0960129508007202_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_20"},{"key":"S0960129508007202_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90068-5"},{"key":"S0960129508007202_ref27","doi-asserted-by":"crossref","unstructured":"Orejas F. (2008) Attributed graph constraints. In: Graph Transformations (ICGT'08). To appear in Springer-Verlag Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-540-87405-8_19"},{"key":"S0960129508007202_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78743-3_14"},{"key":"S0960129508007202_ref30","doi-asserted-by":"crossref","unstructured":"Pennemann K.-H. (2008b) Resolution-like theorem proving for high-level conditions. In: Graph Transformations (ICGT'08). To appear in Springer-Verlag Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-540-87405-8_20"},{"key":"S0960129508007202_ref33","first-page":"569","article-title":"The impossibility of an algorithm for the decision problem on finite classes (in Russian)","volume":"70","author":"Trakhtenbrot","year":"1950","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0960129508007202_ref3","article-title":"ENFORCe: A system for ensuring formal correctness of high-level programs. In: Proc. 3rd. Int. Workshop on Graph Based Tools (GraBaTs'06)","volume":"1","author":"Azab","year":"2006","journal-title":"Electronic Communications of the EASST"},{"key":"S0960129508007202_ref14","first-page":"1","article-title":"Adhesive high-level replacement systems: A new categorical framework for graph transformation","volume":"74","author":"Ehrig","year":"2006","journal-title":"Fundamenta Informaticae"},{"key":"S0960129508007202_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001353"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508007202","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,14]],"date-time":"2020-05-14T16:07:35Z","timestamp":1589472455000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508007202\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["S0960129508007202"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508007202","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4]]}}}