Automating Test Case Generation from Z Specifications with Isabelle

We use a structure preserving encoding of Z in the higher-order logic instance of the generic theorem prover Isabelle to derive test cases from Z specifications. This work shows how advanced theorem provers can be used with little effort to provide tool support for Z beyond mere type-checking. Experience with a non-trivial example shows that modular reasoning according to the structure of a specification is crucial to keep the proof-load manageable in practical applications. Support for modular reasoning can be based on higher-order equational reasoning as implemented in Isabelle