2026-08-10T12:07:51Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5977 2024-03-06T10:37:25Z ddc:004 open_access

Proving Correctness of Logically Decorated Graph Rewriting Systems Brenas, Jon Haël Echahed, Rachid Strecker, Martin Graph Rewriting Hoare Logic,Combinatory PDL Rewrite Strategies Program Verification We first introduce the notion of logically decorated rewriting systems where the left-hand sides are endowed with logical formulas which help to express positive as well as negative application conditions, in addition to classical pattern-matching. These systems are defined using graph structures and an extension of combinatory propositional dynamic logic, CPDL, with restricted universal programs, called C2PDL. In a second step, we tackle the problem of proving the correctness of logically decorated graph rewriting systems by using a Hoare-like calculus. We introduce a notion of specification defined as a tuple (Pre, Post, R, S) with Pre and Post being formulas of C2PDL, R a rewriting system and S a rewriting strategy. We provide a sound calculus which infers proof obligations of the considered specifications and establish the decidability of the verification problem of the (partial) correctness of the considered specifications. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jon Haël Brenas and Rachid Echahed and Martin Strecker 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.14 urn:nbn:de:0030-drops-59778 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.14 eng https://creativecommons.org/licenses/by/3.0/legalcode