Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
9-2012
Abstract
GP 2 is an experimental nondeterministic programming language based on graph transformation rules, allowing for visual programming and the solving of graph problems at a high-level of abstraction. In previous work we demonstrated how to verify graph programs using a Hoare-style proof calculus, but only partial correctness was considered. In this paper, we add new proof rules and termination functions, which allow for proofs to additionally guarantee that program executions always terminate (weak total correctness), or that programs always terminate and do so without failure (total correctness). We show that the new proof rules are sound with respect to the operational semantics of GP 2, complete for termination, and demonstrate their use on some example programs.
Keywords
Graph theory, Graph programs, Hoare logic, Termination, Total correctness, Verification
Discipline
Theory and Algorithms
Research Areas
Software and Cyber-Physical Systems
Publication
Selected revised papers from the 4th International Workshop on Graph Computation Models (GCM 2012): Bremen, Germany, September 28-29
First Page
1
Last Page
20
Identifier
10.14279/tuj.eceasst.61.827
Publisher
EASST
City or Country
Utrecht
Citation
POSKITT, Christopher M. and PLUMP, Detlef.
Verifying total correctness of graph programs. (2012). Selected revised papers from the 4th International Workshop on Graph Computation Models (GCM 2012): Bremen, Germany, September 28-29. 1-20.
Available at: https://ink.library.smu.edu.sg/sis_research/4916
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.14279/tuj.eceasst.61.827