eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-06-17
14:1
14:15
10.4230/LIPIcs.FSCD.2016.14
article
Proving Correctness of Logically Decorated Graph Rewriting Systems
Brenas, Jon Haël
Echahed, Rachid
Strecker, Martin
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol052-fscd2016/LIPIcs.FSCD.2016.14/LIPIcs.FSCD.2016.14.pdf
Graph Rewriting
Hoare Logic,Combinatory PDL
Rewrite Strategies
Program Verification