Title: Stepwise development from ideal specifications
Abstract: The stepwise development of a program using refinement requires that the original abstract specification is realisable, i.e., an implementation exists with identical functionality. In some situations, this may not be desirable or even possible, and an ideal specification which is only approximated by the final implementation is used. For these specifications, an informal step, based on the developer's knowledge and experience, is typically used during the refinement process in order to transform the specification to one which is realisable. This paper introduces a formal approach to such specification transformations called realisation. It enables a specification to be transformed to another with different functionality and, at the same time, allows properties of the new specification to be derived from those of the original.
Publication Year: 2002
Publication Date: 2002-11-07
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 9
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot