[TYPES] Completeness of powersimulation
Malcolm.Tyrrell at computing.dcu.ie
Tue Jul 17 10:25:55 EDT 2007
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 
and reworked in ), 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
The language of  (p223) gives the impression that the conditions are
necessary. However, this is not clearly stated.
 "A Single Complete Rule for Data Refinement", Paul H. B. Gardiner
and Carroll Morgan, Formal Asp. Comput. 1993
 "Data Refinement: Model-Oriented Proof Methods and Their
Comparison", W. de Roever and Kai Engelhardt, Cambridge University
Thanks for any help,
More information about the Types-list