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)

    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
    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
    PublisherSpringer
    Pages445-460
    Number of pages16
    ISBN (Electronic)978-3-540-38872-2
    ISBN (Print)3-540-38870-2
    DOIs
    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
    PublisherSpringer
    Volume4178
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference3rd International Conference on Graph Transformations, ICGT 2006
    Abbreviated titleICGT
    CountryBrazil
    CityNatal
    Period19/09/0621/09/06

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

    Cite this