The stepwise development of a program using refinement requires that the original abstract specification is realizable, 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 realizable.This paper introduces a formal approach to such specification transformations called realization. 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. Used in conjunction with refinement, realization provides a formal and auditable procedure for stepwise development of systems from ideal specifications.
Index Terms:
formal specification, refinement, stepwise development
Citation:
Graeme Smith, "Stepwise Development from Ideal Specifications," acsc, pp.227, Australasian Computer Science Conference, 2000