[TYPES] Completeness of powersimulation

Malcolm Tyrrell Malcolm.Tyrrell at computing.dcu.ie
Tue Jul 17 10:25:55 EDT 2007

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 

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

[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,


More information about the Types-list mailing list