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

      Specification and Refinement in General Correctness

      proceedings-article

      1 , 2 , 1

      3rd BCS-FACS Northern Formal Methods Workshop (NFM)

      BCS-FACS Northern Formal Methods Workshop

      14-15 September 1998

      Bookmark

            Abstract

            We augment B’s existing total-correctness semantics of weakest precondition (wp) with a partial-correctness semantics of weakest liberal precondition (wlp). By so doing we achieve a general-correctness semantics for B operations which not only accords more fully with our natural computational intuition, but also extends the essential expressive capability of B’s Generalised Substitution Language (GSL) to embrace a whole new class of operations called semi-decidable , whose behaviour cannot be characterised in terms of total correctness alone. The ability to specify semi-decidable operations is important because a desired conventional operation may lend itself to implementation as a concurrent federation of semi-decidable operations co-operating under a mutual “termination pact”. Indeed, computational constraints may render this the only viable implementation strategy. We call a generalised substi- tution invested with our general-correctness semantics an abstract command . Our Abstract Command Language (ACL) is thus syntactically indistinguishable from the GSL, save for the introduction of one new composition operator, concert , expressing a “termination pact” between two concurrent abstract commands.

            Content

            Author and article information

            Conference
            September 1998
            September 1998
            : 1-19
            Affiliations
            [0001]School of Computing and Mathematics, University of Teesside
            [0002]High Integrity Systems Engineering Group, University of York
            Article
            10.14236/ewic/NFM1998.8
            a16fa9ad-e81e-4002-82d8-4796818d0152
            © Steve Dunne et al. Published by BCS Learning and Development Ltd. 3rd BCS-FACS Northern Formal Methods Workshop, Ilkley, 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/

            3rd BCS-FACS Northern Formal Methods Workshop
            NFM
            3
            Ilkley, UK
            14-15 September 1998
            Electronic Workshops in Computing (eWiC)
            BCS-FACS Northern Formal Methods Workshop
            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