Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
8-2010
Abstract
We present a new approach for verifying programs written in GP (for Graph Programs), an experimental programming language for performing computations on graphs at a high level of abstraction. Taking a labelled graph as input, a graph program nondeterministically applies to it a number of graph transformation rules, directed by simple control constructs such as sequential composition and as-long-as-possible iteration. We adapt classical Hoare logic to the domain of graphs, and describe a system of sound proof rules for showing the partial correctness of graph programs.
Discipline
Theory and Algorithms
Research Areas
Software and Cyber-Physical Systems
Publication
VSTTE 2010 Workshop Proceedings: Edinburgh, August 16-19
First Page
1
Last Page
11
Identifier
10.3929/ethz-a-006860117
Publisher
ETH
City or Country
Zurich
Citation
POSKITT, Christopher M. and PLUMP, Detlef.
Hoare logic for graph programs. (2010). VSTTE 2010 Workshop Proceedings: Edinburgh, August 16-19. 1-11.
Available at: https://ink.library.smu.edu.sg/sis_research/4921
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.3929/ethz-a-006860117