Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    IO-Refinement in Z

    3rd BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 14th - 15th September 1998


    E. Boiten & J. Derrick


    We present a generalisation of data refinement in Z, called IO-refinement, that allows changes in input and output parameters of operations.

    Several informal motivations for the desirability of such a refinement relation are given, followed by a formal derivation that demonstrates its theoretical soundness.

    It is proved that IO-refinement indeed generalizes data refinement. Several theorems are presented that give sufficient conditions for IO-refinement to hold in simpler situations, e.g. just adding inputs and outputs.

    Some examples of the use of IO-refinement are also given.


    PDF filePDF Version of this Paper (192kb)