Reasoning about Graph Programs

Detlef  Plump

doi:10.4204/EPTCS.225.6

Reasoning about Graph Programs

Detlef Plump

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with four case studies how programmers can prove termination and partial correctness of their solutions. We argue that GP 2's graph transformation rules, together with induction over the length of program executions, provide a convenient framework for program verification.

Original language	English
Title of host publication	Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016)
Editors	Andrea Corradini, Hans Zantema
Publisher	Open Publishing Association
Pages	35-44
Number of pages	10
Volume	225
DOIs	https://doi.org/10.4204/EPTCS.225.6
Publication status	Published - 2016

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Volume	225

Bibliographical note

Publisher Copyright:
© D. Plump.

Access to Document

10.4204/EPTCS.225.6

Plump.TG.16Final published version, 106 KBLicence: CC BY

http://www.cs.york.ac.uk/plasma/publications/pdf/Plump.TG.16.pdf

Cite this

@inproceedings{6d8cff2b6f90440cbca83257a663a60e,

title = "Reasoning about Graph Programs",

abstract = "GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with four case studies how programmers can prove termination and partial correctness of their solutions. We argue that GP 2's graph transformation rules, together with induction over the length of program executions, provide a convenient framework for program verification.",

author = "Detlef Plump",

note = "Publisher Copyright: {\textcopyright} D. Plump.",

year = "2016",

doi = "10.4204/EPTCS.225.6",

language = "English",

volume = "225",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "35--44",

editor = "Andrea Corradini and Hans Zantema",

booktitle = "Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016)",

address = "Australia",

}

Reasoning about Graph Programs. / Plump, Detlef .
Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016). ed. / Andrea Corradini; Hans Zantema. Vol. 225 Open Publishing Association, 2016. p. 35-44 (Electronic Proceedings in Theoretical Computer Science; Vol. 225).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Reasoning about Graph Programs

AU - Plump, Detlef

PY - 2016

Y1 - 2016

N2 - GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with four case studies how programmers can prove termination and partial correctness of their solutions. We argue that GP 2's graph transformation rules, together with induction over the length of program executions, provide a convenient framework for program verification.

AB - GP 2 is a non-deterministic programming language for computing by graph transformation. One of the design goals for GP 2 is syntactic and semantic simplicity, to facilitate formal reasoning about programs. In this paper, we demonstrate with four case studies how programmers can prove termination and partial correctness of their solutions. We argue that GP 2's graph transformation rules, together with induction over the length of program executions, provide a convenient framework for program verification.

UR - http://www.scopus.com/inward/record.url?scp=85015958160&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.225.6

DO - 10.4204/EPTCS.225.6

M3 - Conference contribution

VL - 225

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 35

EP - 44

BT - Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016)

A2 - Corradini, Andrea

A2 - Zantema, Hans

PB - Open Publishing Association

ER -

Reasoning about Graph Programs

Abstract

Publication series

Bibliographical note

Access to Document

Other files and links

Cite this