Weakest Preconditions for High-Level Programs

Annegret Habel, Karl-Heinz Pennemann, Arend Rensink

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    23 Downloads (Pure)


    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
    Title of host publicationGraph Transformations (ICGT)
    Subtitle of host publicationThird International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings
    EditorsAndrea Corradini, Hartmut Ehrig, Ugo Montanari, Leila Ribeiro, Grzegorz Rozenberg
    Place of PublicationBerlin
    Number of pages16
    ISBN (Electronic)978-3-540-38872-2
    ISBN (Print)3-540-38870-2
    Publication statusPublished - Sep 2006
    Event3rd International Conference on Graph Transformations, ICGT 2006 - Natal, Brazil
    Duration: 19 Sep 200621 Sep 2006
    Conference number: 3

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference3rd International Conference on Graph Transformations, ICGT 2006
    Abbreviated titleICGT

    Fingerprint Dive into the research topics of 'Weakest Preconditions for High-Level Programs'. Together they form a unique fingerprint.

    Cite this