Performing algorithmic refinement before data refonement in B

Butler, Michael and Meagher, Mairead (2000) Performing algorithmic refinement before data refonement in B. In: ZB 2000 : Formal Specification and Development in Z and B - 1st International Conference of B and Z Users, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . Springer Verlag, GBR, pp. 324-343. ISBN 9783540679448

Full text not available from this repository. (Request a copy)


Algorithmic Refinement is part of the theory of the B method both at the refinement and implementation stages. It a sign of how little loop introduction is used in practice at the refinement stage that neither the B-Toolkit nor Atelier-B provide support for loop introduction until the implementation stage. This paper examines the use of algorithmic refinement in general before data refinement. This involves extending the usual scope of data refinement which usually happens before algorithmic refinement. Two case studies are used to compare and contrast the application of algorithmic refinement before data refinement and vice versa. Some extensions are needed in the B-Toolkit to implement this style (i.e., algorithmic before data refinement) and are proposed. Some workarounds are also presented when appropriate.

Item Type: Book Section
Additional Information: Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2000.
Uncontrolled Keywords: /dk/atira/pure/subjectarea/asjc/2600/2614
Departments or Groups:
Depositing User: Admin SSL
Date Deposited: 19 Oct 2022 23:16
Last Modified: 07 Jun 2023 18:39

Actions (login required)

View Item View Item