Weakest Preconditions for High-Level Programs


Habel, Annegret and Pennemann, Karl-Heinz and Rensink, Arend (2006) Weakest Preconditions for High-Level Programs. In: Third International Conference on Graph Transformations, ICGT 2006, 19-21 September 2006, Natal, Rio Grande do Norte, Brazil (pp. pp. 445-460).

open access
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.
Item Type:Conference or Workshop Item
Copyright:© 2006 Springer
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/65587
Official URL:https://doi.org/10.1007/11841883_31
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 237999