Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
9-2010
Abstract
We present Hoare-style axiom schemata and inference rules for verifying the partial correctness of programs in the graph programming language GP. The pre- and postconditions of this calculus are the nested conditions of Habel, Pennemann and Rensink, extended with expressions for labels in order to deal with GP’s conditional rule schemata and infinite label alphabet. We show that the proof rules are sound with respect to GP’s operational semantics.
Keywords
Inference Rule, Proof System, Graph Transformation, Graph Program, Partial Correctness
Discipline
Theory and Algorithms
Research Areas
Software and Cyber-Physical Systems
Publication
Graph Transformations: 5th International Conference, ICGT 2010, Enschede, the Netherlands, September 27-October 2, Proceedings
Volume
6372
First Page
139
Last Page
154
ISBN
9783642159282
Identifier
10.1007/978-3-642-15928-2_10
Publisher
Springer
City or Country
Berlin
Citation
POSKITT, Christopher M. and PLUMP, Detlef.
A Hoare calculus for graph programs. (2010). Graph Transformations: 5th International Conference, ICGT 2010, Enschede, the Netherlands, September 27-October 2, Proceedings. 6372, 139-154.
Available at: https://ink.library.smu.edu.sg/sis_research/4918
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-642-15928-2_10