Weakest Preconditions for High-Level Programs

Annegret Habel, Karl-Heinz Pennemann, Arend Rensink

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

    15 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

    Precondition
    Proof Theory
    Correctness
    Imply
    Graph in graph theory

    Cite this

    Habel, A., Pennemann, K-H., & Rensink, A. (2006). Weakest Preconditions for High-Level Programs. In A. Corradini, H. Ehrig, U. Montanari, L. Ribeiro, & G. Rozenberg (Eds.), Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings (pp. 445-460). (Lecture Notes in Computer Science; Vol. 4178). Berlin: Springer. https://doi.org/10.1007/11841883_31
    Habel, Annegret ; Pennemann, Karl-Heinz ; Rensink, Arend. / Weakest Preconditions for High-Level Programs. Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. editor / Andrea Corradini ; Hartmut Ehrig ; Ugo Montanari ; Leila Ribeiro ; Grzegorz Rozenberg. Berlin : Springer, 2006. pp. 445-460 (Lecture Notes in Computer Science).
    @inproceedings{8a539d57cee140f9aac7c2754ae797c9,
    title = "Weakest Preconditions for High-Level Programs",
    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.",
    author = "Annegret Habel and Karl-Heinz Pennemann and Arend Rensink",
    year = "2006",
    month = "9",
    doi = "10.1007/11841883_31",
    language = "English",
    isbn = "3-540-38870-2",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "445--460",
    editor = "Andrea Corradini and Hartmut Ehrig and Ugo Montanari and Leila Ribeiro and Grzegorz Rozenberg",
    booktitle = "Graph Transformations (ICGT)",

    }

    Habel, A, Pennemann, K-H & Rensink, A 2006, Weakest Preconditions for High-Level Programs. in A Corradini, H Ehrig, U Montanari, L Ribeiro & G Rozenberg (eds), Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. Lecture Notes in Computer Science, vol. 4178, Springer, Berlin, pp. 445-460, 3rd International Conference on Graph Transformations, ICGT 2006, Natal, Brazil, 19/09/06. https://doi.org/10.1007/11841883_31

    Weakest Preconditions for High-Level Programs. / Habel, Annegret; Pennemann, Karl-Heinz; Rensink, Arend.

    Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. ed. / Andrea Corradini; Hartmut Ehrig; Ugo Montanari; Leila Ribeiro; Grzegorz Rozenberg. Berlin : Springer, 2006. p. 445-460 (Lecture Notes in Computer Science; Vol. 4178).

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

    TY - GEN

    T1 - Weakest Preconditions for High-Level Programs

    AU - Habel, Annegret

    AU - Pennemann, Karl-Heinz

    AU - Rensink, Arend

    PY - 2006/9

    Y1 - 2006/9

    N2 - 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.

    AB - 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.

    U2 - 10.1007/11841883_31

    DO - 10.1007/11841883_31

    M3 - Conference contribution

    SN - 3-540-38870-2

    T3 - Lecture Notes in Computer Science

    SP - 445

    EP - 460

    BT - Graph Transformations (ICGT)

    A2 - Corradini, Andrea

    A2 - Ehrig, Hartmut

    A2 - Montanari, Ugo

    A2 - Ribeiro, Leila

    A2 - Rozenberg, Grzegorz

    PB - Springer

    CY - Berlin

    ER -

    Habel A, Pennemann K-H, Rensink A. Weakest Preconditions for High-Level Programs. In Corradini A, Ehrig H, Montanari U, Ribeiro L, Rozenberg G, editors, Graph Transformations (ICGT): Third International Conference, ICGT 2006 Natal, Rio Grande do Norte, Brazil, September 17-23, 2006: Proceedings. Berlin: Springer. 2006. p. 445-460. (Lecture Notes in Computer Science). https://doi.org/10.1007/11841883_31