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. © Springer-Verlag Berlin Heidelberg 2006.
Cite
CITATION STYLE
Habel, A., Pennemann, K. H., & Rensink, A. (2006). Weakest preconditions for high-level programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4178 LNCS, pp. 445–460). Springer Verlag. https://doi.org/10.1007/11841883_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
