[TYPES] Completeness of powersimulation

[Malcolm Tyrrell]

Hi there.

I'm not sure that this is the appropriate forum for my question, so I 
apologise if it seems off-topic. If you can think of a more suitable 
forum, please tell me.

Powersimulation is a sound technique for establishing data refinement in 
theories of predicate transformers.

There is a completeness result for powersimulation (originally in [1] 
and reworked in [2]), but it is subject to a few awkward conditions. In 
particular, abstract data types may not use unbounded nondeterminacy.

Can anyone tell me if it is known whether the conditions are necessary?
If not, can anyone provide an example of the incompleteness of 
powersimulation?

The language of [2] (p223) gives the impression that the conditions are 
necessary. However, this is not clearly stated.

References:
[1] "A Single Complete Rule for Data Refinement", Paul H. B. Gardiner 
and Carroll Morgan, Formal Asp. Comput. 1993

[2] "Data Refinement: Model-Oriented Proof Methods and Their 
Comparison", W. de Roever and Kai Engelhardt, Cambridge University 
Press, 1999

Thanks for any help,

Malcolm.