Performing algorithmic refinement before data refonement in B

Michael Butler, Mairead Meagher

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationZB 2000
Subtitle of host publicationFormal Specification and Development in Z and B - 1st International Conference of B and Z Users, Proceedings
EditorsJonathan P. Bowen, Steve Dunne, Andy Galloway, Steve King
PublisherSpringer
Pages324-343
Number of pages20
ISBN (Electronic)9783540679448
DOIs
Publication statusPublished - 2000
Event1st International Conference of B and Z Users, ZB 2000 - York, United Kingdom
Duration: 29 Aug 200002 Sep 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1878
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference1st International Conference of B and Z Users, ZB 2000
Country/TerritoryUnited Kingdom
CityYork
Period29/08/200002/09/2000

Fingerprint

Dive into the research topics of 'Performing algorithmic refinement before data refonement in B'. Together they form a unique fingerprint.

Cite this