Derivation of Z functional input/output refinement proof rules

In this paper, we derive Z input/output data refinement rules, including forwards and backwards rules, for the case in which the retrieve schemas are total functions when viewed as relations from the concrete to abstract variables. In practice, the relation between the abstract and concrete variables is often functional. Therefore, the use of the functional input/output refinement rules will reduce the cost and duration of the software development because the proof of the consistency of the abstract and concrete specifications is more easily demonstrated.