CSM-364 - An analysis of operation refinement in Z
Martin C. Henson, Moshe Deutsch, Steve Reeves · Open Access at Essex (University of Essex) · 2002
In this paper we analyse and compare several notions of operation refinement for specifications in Z. In particular we show that three theories: relational completion, proof-theoretic and functional (models) are all equivalent.