Weakest Preconditions for High-Level Programs

Annegret Habel; Karl-Heinz Pennemann; Arend Rensink

doi:10.1007/11841883_31

Weakest Preconditions for High-Level Programs

Annegret Habel, Karl-Heinz Pennemann, Arend Rensink

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

56 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 language	English
Title of host publication	Graph Transformations (ICGT)
Subtitle of host publication	Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings
Editors	Andrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, Grzegorz Rozenberg
Place of Publication	Berlin
Publisher	Springer
Pages	445-460
Number of pages	16
ISBN (Electronic)	978-3-540-38872-2
ISBN (Print)	3-540-38870-2
DOIs	https://doi.org/10.1007/11841883_31
Publication status	Published - Sept 2006
Event	3rd International Conference on Graph Transformations, ICGT 2006 - Natal, Brazil Duration: 19 Sept 2006 → 21 Sept 2006 Conference number: 3

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4178
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Conference on Graph Transformations, ICGT 2006
Abbreviated title	ICGT
Country/Territory	Brazil
City	Natal
Period	19/09/06 → 21/09/06

Access to Document

10.1007/11841883_31

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). 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 = sep,

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)",

address = "Germany",

note = "3rd International Conference on Graph Transformations, ICGT 2006, ICGT ; Conference date: 19-09-2006 Through 21-09-2006",

}

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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Weakest Preconditions for High-Level Programs

AU - Habel, Annegret

AU - Pennemann, Karl-Heinz

AU - Rensink, Arend

N1 - Conference code: 3

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

T2 - 3rd International Conference on Graph Transformations, ICGT 2006

Y2 - 19 September 2006 through 21 September 2006

ER -

Habel A, Pennemann KH, 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). doi: 10.1007/11841883_31

Weakest Preconditions for High-Level Programs

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this