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

      Recasting Hoare and He’s Unifying Theory of Programs in the Context of General Correctness

      proceedings-article

      5th Irish Workshop on Formal Methods (IWFM)

      Irish Workshop on Formal Methods

      16-17 July 2001

      Bookmark

            Abstract

            We review Hoare and He’s single-predicate model of sequential programs, and uncover its inability always to provide an adequate description of the required behaviour of a sequential program which implements a partial decision procedure: a significant shortcoming in an interactive era where such programs are often found as components of reactive systems. We show how the single-predicate model can be recast to overcome this limitation, using a variation on the predicate syntactic form employed by Hoare and He for their designs, which we call a prescription . We show that our prescriptions have a remarkably simple semantic characterisation by means of a single intuitively compelling healthiness condition. Our model also admits a pleasingly simple algebraic formulation which reveals it as a natural completion of Hoare and He’s model; indeed, we can show the latter to be congruent to a restricted sub-model of the former.

            Content

            Author and article information

            Contributors
            Conference
            July 2001
            July 2001
            : 1-23
            Affiliations
            [0001]School of Computing and Mathematics, University of Teesside

            Middlesbrough, TS1 3BA, UK
            Article
            10.14236/ewic/IWFM2001.1
            934e2169-eb68-4fdb-8c99-5bcab7e1205d
            © Steve Dunne. Published by BCS Learning and Development Ltd. 5th Irish Workshop on Formal Methods, Dublin, Ireland

            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/

            5th Irish Workshop on Formal Methods
            IWFM
            5
            Dublin, Ireland
            16-17 July 2001
            Electronic Workshops in Computing (eWiC)
            Irish Workshop on Formal Methods
            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