Weakest Preconditions for High-Level Programs (Long Version)

Annegret Habel, Karl-Heinz Pennemann, Arend Rensink

    Research output: Book/ReportReportProfessional

    28 Citations (Scopus)
    43 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 languageEnglish
    Place of PublicationOldenburg
    PublisherUniversity of Oldenburg
    Number of pages35
    Publication statusPublished - Jul 2006

    Publication series

    NameBerichte aus dem Department für Informatik
    PublisherUniversity of Oldenburg
    No.8/06
    ISSN (Print)0946-2910

      Fingerprint

    Cite this

    Habel, A., Pennemann, K-H., & Rensink, A. (2006). Weakest Preconditions for High-Level Programs (Long Version). (Berichte aus dem Department für Informatik; No. 8/06). Oldenburg: University of Oldenburg.