A Hoare calculus for graph programs

A Hoare calculus for graph programs

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 d...

Full description

Saved in:
Bibliographic Details
Main Authors: POSKITT, Christopher M., PLUMP, Detlef
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2010
Subjects:
Inference Rule
Proof System
Graph Transformation
Graph Program
Partial Correctness
Theory and Algorithms
Online Access:https://ink.library.smu.edu.sg/sis_research/4918
https://ink.library.smu.edu.sg/context/sis_research/article/5921/viewcontent/PoskittPlump.ICGT.2010.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary: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.

Similar Items