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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Poskitt, C. M., & Plump, D. (2010). A Hoare calculus for graph programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6372 LNCS, pp. 139–154). https://doi.org/10.1007/978-3-642-15928-2_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
