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

      Separating Algorithm and Implementation in the Refinement of Parallel Program Specifications

      proceedings-article

      Proceedings of the BCS-FACS 7th Refinement Workshop (RW)

      BCS-FACS 7th Refinement Workshop

      3-5 July 1996

      Bookmark

            Abstract

            Correct concurrent programs can be obtained through the refinement of abstract specifications. In this paper, we explore a methodology, which we call task separation , in which we split the development of a program in two phases: a first stage where an algorithm is introduced from a TLA + specification, but where the data structures remain unconstrained; a second stage where the other aspects of the program are dealt with. The intermediate state can be represented in an object-oriented way, emphasizing its relationship with languages like C++. This notation, cTLA (concrete TLA) is defined semantically in TLA + and aims to provide a fair representation of an algorithm, compared to TLA + ’s at rendering. cTLA’s types and values are the values in TLA+. cTLA’s class instances are processes, and there are virtually an infinite number of processes, which can be activated. A numerical example, the block decomposition algorithm in the matrix multiplication, supports our views.

            Content

            Author and article information

            Contributors
            Conference
            July 1996
            July 1996
            : 1-21
            Affiliations
            [0001]CRIN

            Bâtiment LORIA

            Campus scientifique — BP 239

            54506 Vandœuvre-lès-Nancy cedex, France
            Article
            10.14236/ewic/RW1996.12
            b40f8041-f485-4e8b-aa65-d74a42e1868b
            © Denis Roegel. Published by BCS Learning and Development Ltd. Proceedings of the BCS-FACS 7th Refinement Workshop, Bath

            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/

            Proceedings of the BCS-FACS 7th Refinement Workshop
            RW
            7
            Bath
            3-5 July 1996
            Electronic Workshops in Computing (eWiC)
            BCS-FACS 7th Refinement 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