Weakest Preconditions for High-Level Programs

Annegret Habel, Karl-Heinz Pennemann, Arend Rensink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

14 Downloads (Pure)

Abstract

In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented.
Original languageEnglish
Title of host publicationGraph Transformations (ICGT)
Subtitle of host publicationThird International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings
EditorsAndrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, Grzegorz Rozenberg
Place of PublicationBerlin
PublisherSpringer
Pages445-460
Number of pages16
ISBN (Electronic)978-3-540-38872-2
ISBN (Print)3-540-38870-2
DOIs
Publication statusPublished - Sep 2006
Event3rd International Conference on Graph Transformations, ICGT 2006 - Natal, Brazil
Duration: 19 Sep 200621 Sep 2006
Conference number: 3

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume4178
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Conference on Graph Transformations, ICGT 2006
Abbreviated titleICGT
CountryBrazil
CityNatal
Period19/09/0621/09/06

Fingerprint

Precondition
Proof Theory
Correctness
Imply
Graph in graph theory

Cite this

Habel, A., Pennemann, K-H., & Rensink, A. (2006). Weakest Preconditions for High-Level Programs. In A. Corradini, H. Ehrig, U. Montanari, L. Ribeiro, & G. Rozenberg (Eds.), Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings (pp. 445-460). (Lecture Notes in Computer Science; Vol. 4178). Berlin: Springer. https://doi.org/10.1007/11841883_31
Habel, Annegret ; Pennemann, Karl-Heinz ; Rensink, Arend. / Weakest Preconditions for High-Level Programs. Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. editor / Andrea Corradini ; Hartmut Ehrig ; Ugo Montanari ; Leila Ribeiro ; Grzegorz Rozenberg. Berlin : Springer, 2006. pp. 445-460 (Lecture Notes in Computer Science).
@inproceedings{8a539d57cee140f9aac7c2754ae797c9,
title = "Weakest Preconditions for High-Level Programs",
abstract = "In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented.",
author = "Annegret Habel and Karl-Heinz Pennemann and Arend Rensink",
year = "2006",
month = "9",
doi = "10.1007/11841883_31",
language = "English",
isbn = "3-540-38870-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "445--460",
editor = "Andrea Corradini and Hartmut Ehrig and Ugo Montanari and Leila Ribeiro and Grzegorz Rozenberg",
booktitle = "Graph Transformations (ICGT)",

}

Habel, A, Pennemann, K-H & Rensink, A 2006, Weakest Preconditions for High-Level Programs. in A Corradini, H Ehrig, U Montanari, L Ribeiro & G Rozenberg (eds), Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. Lecture Notes in Computer Science, vol. 4178, Springer, Berlin, pp. 445-460, 3rd International Conference on Graph Transformations, ICGT 2006, Natal, Brazil, 19/09/06. https://doi.org/10.1007/11841883_31

Weakest Preconditions for High-Level Programs. / Habel, Annegret; Pennemann, Karl-Heinz; Rensink, Arend.

Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. ed. / Andrea Corradini; Hartmut Ehrig; Ugo Montanari; Leila Ribeiro; Grzegorz Rozenberg. Berlin : Springer, 2006. p. 445-460 (Lecture Notes in Computer Science; Vol. 4178).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Weakest Preconditions for High-Level Programs

AU - Habel, Annegret

AU - Pennemann, Karl-Heinz

AU - Rensink, Arend

PY - 2006/9

Y1 - 2006/9

N2 - In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented.

AB - In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented.

U2 - 10.1007/11841883_31

DO - 10.1007/11841883_31

M3 - Conference contribution

SN - 3-540-38870-2

T3 - Lecture Notes in Computer Science

SP - 445

EP - 460

BT - Graph Transformations (ICGT)

A2 - Corradini, Andrea

A2 - Ehrig, Hartmut

A2 - Montanari, Ugo

A2 - Ribeiro, Leila

A2 - Rozenberg, Grzegorz

PB - Springer

CY - Berlin

ER -

Habel A, Pennemann K-H, Rensink A. Weakest Preconditions for High-Level Programs. In Corradini A, Ehrig H, Montanari U, Ribeiro L, Rozenberg G, editors, Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. Berlin: Springer. 2006. p. 445-460. (Lecture Notes in Computer Science). https://doi.org/10.1007/11841883_31