Liberating data refinement

Boiten, Eerke and Derrick, John (2000) Liberating data refinement. In: Backhouse, Roland C. and Oliveira, Jose Nuno, eds. Proceedings of the 5th International Conference on Mathematics of Program Construction. Lecture Notes in Computer Science, 1837. Springer pp. 144-166. ISBN 3-540-67727-5. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://dx.doi.org/10.1007/10722010_11

Abstract

Traditional rules for refinement of abstract data types suggest a software development process in which much of the detail has to be present already in the initial specification. In particular, the set of available operations and their interfaces need to be fixed. In contrast, many formal and informal software development methods rely on changes of granularity and require introduction of detail in a gradual way during the development process. This paper discusses several generalisations and extensions of the traditional refinement rules, which are compatible with each other and, more importantly, with the semantic grounding of data refinement. Together they should provide a semantic justification to a larger spectrum of development steps. The discussion takes place in the context of the formal specification language Z and its relational underpinnings.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Refinement, formal methods, Z
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Mark Wheadon
Date Deposited: 09 Sep 2009 12:53
Last Modified: 13 May 2014 08:33
Resource URI: http://kar.kent.ac.uk/id/eprint/22003 (The current URI for this page, for reference purposes)
  • Depositors only (login required):