Z Toolkit

The Z notation is an ISO standard (13568:2002) for formal specifications, based on set theory and relations. Z comes with a mathematical toolkit, which can be used in the formation of specifications.

We have implemented the core types of Z in Isabelle/HOL, such a partial functions and finite injections, together with a large and growing library of theorems. We reuse types from HOL as much as possible (e.g. lists), and add further definitions and theorems for compatibility with the toolkit, where necessary. Thanks to Isabelle's flexible unicode font (and Makarius Wenzel for supporting this), we can support all mathematical symbols in Z.

We can then form store types using a notation similar to state schemas, as seen in the accompanying image. Such state declarations are used in various tools, including imperative programs and Z Machines. For details on the implementation, please see the Z_Toolkit Git repository.