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...
Saved in:
Main Authors: | POSKITT, Christopher M., PLUMP, Detlef |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2010
|
Subjects: | |
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 |
Similar Items
-
Verifying monadic second-order properties of graph programs
by: POSKITT, Christopher M., et al.
Published: (2014) -
Verifying total correctness of graph programs
by: POSKITT, Christopher M., et al.
Published: (2012) -
Hoare logic for graph programs
by: POSKITT, Christopher M., et al.
Published: (2010) -
Verification of graph programs
by: POSKITT, Christopher M.
Published: (2012) -
Monadic second-order incorrectness logic for GP 2
by: POSKITT, Christopher M., et al.
Published: (2023)