State-level and value-level simulations in data refinement

Simulations are a popular way to show data refinement. Simulations that hav e been proposed are either state-level, relating concrete to abstract state s in a given state space, or value-level, relating individual concrete to a bstract values and hence holding for all state spaces, value-level simulati ons are less complex and easier to use, but the extent of their completenes s has not been well studied. We show that in fact known value-level simulat ions are in general incomplete but are complete when operations are limited to a single argument. (C) 2001 Elsevier Science B.V. All rights reserved.