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

id	sg-smu-ink.sis_research-5921
record_format	dspace
spelling	sg-smu-ink.sis_research-59212020-02-13T06:58:56Z A Hoare calculus for graph programs POSKITT, Christopher M. PLUMP, Detlef 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-09-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4918 info:doi/10.1007/978-3-642-15928-2_10 https://ink.library.smu.edu.sg/context/sis_research/article/5921/viewcontent/PoskittPlump.ICGT.2010.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Inference Rule Proof System Graph Transformation Graph Program Partial Correctness Theory and Algorithms
institution	Singapore Management University
building	SMU Libraries
continent	Asia
country	Singapore Singapore
content_provider	SMU Libraries
collection	InK@SMU
language	English
topic	Inference Rule Proof System Graph Transformation Graph Program Partial Correctness Theory and Algorithms
spellingShingle	Inference Rule Proof System Graph Transformation Graph Program Partial Correctness Theory and Algorithms POSKITT, Christopher M. PLUMP, Detlef A Hoare calculus for graph programs
description	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.
format	text
author	POSKITT, Christopher M. PLUMP, Detlef
author_facet	POSKITT, Christopher M. PLUMP, Detlef
author_sort	POSKITT, Christopher M.
title	A Hoare calculus for graph programs
title_short	A Hoare calculus for graph programs
title_full	A Hoare calculus for graph programs
title_fullStr	A Hoare calculus for graph programs
title_full_unstemmed	A Hoare calculus for graph programs
title_sort	hoare calculus for graph programs
publisher	Institutional Knowledge at Singapore Management University
publishDate	2010
url	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
_version_	1770575095110041600

A Hoare calculus for graph programs

Similar Items