Open AccessIO-refinement in Z
Author(s) -
Eerke Boiten,
John Derrick
Publication year - 1998
Publication title -
electronic workshops in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 1477-9358
DOI - 10.14236/ewic/nfm1998.3
Subject(s) - soundness , refinement calculus , computer science , relation (database) , refinement , algorithm , theoretical computer science , algebra over a field , programming language , formal verification , mathematics , data mining , pure mathematics
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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom