Weakest Preconditions for High-Level Programs (Long Version)
Annegret Habel, Karl‐Heinz Pennemann, Arend Rensink · University of Twente Research Information · 2006
Abstract. In proof theory, a standard method for showing the correct-ness 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 Ha-bel 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 con-struction of weakest preconditions is presented. 1