Checking Z Data Refinements Using an Animation Tool

摘要

We describe how a Z animation tool can be used to check Z data refinements. We illustrate two approaches. In the first approach the tool is used to interactively step through operations of the abstract and concrete specifications, checking whether the refinement relationship holds. In the second approach the tool is used to automatically check refinements and to provide counter-examples should the refinement fail. We envisage these techniques being used in order to improve understanding of refinements and to help validate their correctness.