Karl, If I understand the example correctly, yes, I would call this a refinement, in that it extends the set of behaviors of the program. It might, for instance, be possible to show (under the right conditions) that one program simulates or is bisimular to the other. Shriram