Blog
About

133
views
0
recommends
+1 Recommend
1 collections
    4
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Invited Keynote Talk Invariant Based Programming

      Teaching Formal Methods: Practice and Experience (TFM)

      Teaching Formal Methods: Practice and Experience

      15 December 2006

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          There are a few standard approaches to constructing verified programs. The original approach, by Floyd, Naur and Hoare, assumes that the program code is given, together with an informal description of what the program is supposed to do. Program verification amounts to expressing the requirements as precise pre- and postconditions, finding the appropriate loop invariants, constructing the verification conditions and proving them correct. This is known as a posteriori verification. Dijkstra popularized an alternative approach, correct-by-construction, where we also start by formulating precise pre- and postconditions. Program code and loop invariants are then derived at the same time, hand in hand, and verification conditions are proved as they arise. The third possibility, invariant based programming (Reynolds, van Emden, Back, see [1]), moves the construction of program code to an even later stage. Pre- and postconditions are formulated first, as in the other approaches. The next step is then to formulate the loop invariants, before any code is written. The code is constructed last, as transitions between the different situations (precondition, postcondition, loop invariants) that can occur during program execution. The verification conditions corresponding to these transitions are verified as they arise.

          Related collections

          Most cited references 1

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Invariant Based Programming

            Bookmark

            Author and article information

            Contributors
            Conference
            December 2006
            December 2006
            : 1-2
            Affiliations
            Abo Akademi University

            Joukohaisenkatu 3-5, 20520 Turku, Finland

            www.abo.fi/~backrj
            Article
            10.14236/ewic/TFM2006.1
            © Ralph-Johan Back. Published by BCS Learning and Development Ltd. Teaching Formal Methods: Practice and Experience, BCS London Office, UK

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Teaching Formal Methods: Practice and Experience
            TFM
            BCS London Office, UK
            15 December 2006
            Electronic Workshops in Computing (eWiC)
            Teaching Formal Methods: Practice and Experience
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article