An analysis of operation refinement in Z
Moshe Deutsch, Martin C. Henson, Steve Reeves · 2001
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. 1