Operation Refinement takes place within a single specification. One one kind of state space is involved.
It is a way of relating operations defined on the same data.
The concrete operation OpC is a refinement of the abstract operation OpA, both defined on the same state space, iff both of the following formulae can be proved:
- pre OpA ? pre OpC
- the concrete operation succeeds whenever the abstract one does
- pre OpA ? OpC ? OpA
- the abstract and the concrete operations produce the same results on the same starting states.