Monotonic properties are known to be preserved under software refinement, and there are counterexamples when an operator such as negation is introduced. The authors of this paper show that monotonic temporal logic properties are preserved under Z refinement, which is not hard to believe.

One of the points of the analysis is that a “retrieve” function (from the concrete to the abstract) rather than a relation is required in some cases, which appeared in Hoare’s pioneering 1972 paper [1]; de Roever and Engelhardt also deal extensively with this subject in their book [2]. When changing specifications from correctness triples to temporal logic, the completeness arguments in the book do not apply. This paper does not attempt completeness, but only provides examples.