Weakest Preconditions for High-Level Programs (Long Version)

Annegret Habel; Karl-Heinz Pennemann; Arend Rensink

Weakest Preconditions for High-Level Programs (Long Version)

Annegret Habel, Karl-Heinz Pennemann, Arend Rensink

Research output: Book/Report › Report › Professional

37 Citations (Scopus)

77 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
Place of Publication	Oldenburg
Publisher	University of Oldenburg
Number of pages	35
Publication status	Published - Jul 2006

Publication series

Name	Berichte aus dem Department für Informatik
Publisher	University of Oldenburg
No.	8/06
ISSN (Print)	0946-2910

Access to Document

Habel2006weakestFinal published version, 694 KB

http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/hpr-techreport.pdf

Cite this

@book{27ac00f9168347adb6272def99c7b83d,

title = "Weakest Preconditions for High-Level Programs (Long Version)",

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 = jul,

language = "English",

series = "Berichte aus dem Department f{\"u}r Informatik",

publisher = "University of Oldenburg",

number = "8/06",

}

TY - BOOK

T1 - Weakest Preconditions for High-Level Programs (Long Version)

AU - Habel, Annegret

AU - Pennemann, Karl-Heinz

AU - Rensink, Arend

PY - 2006/7

Y1 - 2006/7

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.

M3 - Report

T3 - Berichte aus dem Department für Informatik

BT - Weakest Preconditions for High-Level Programs (Long Version)

PB - University of Oldenburg

CY - Oldenburg

ER -