Blog
About

129
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 of the BCS-FACS 7th Refinement Workshop (RW)

      BCS-FACS 7th Refinement Workshop

      3-5 July 1996

      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

          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.

          Related collections

          Author and article information

          Contributors
          Conference
          July 1996
          July 1996
          : 1-21
          Affiliations
          CRIN

          Bâtiment LORIA

          Campus scientifique — BP 239

          54506 Vandœuvre-lès-Nancy cedex, France
          Article
          10.14236/ewic/RW1996.12
          © 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