Boiten, E.A. and Derrick, J. (2000) Liberating data refinement. In: Backhouse, R.C. and Oliveira, J.N., 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. (Contact us about this Publication)|
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:||09 Sep 2009 12:53|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/22003 (The current URI for this page, for reference purposes)|
- Depositors only (login required):