We harness Isabelle's type system to support state spaces with rich types. In this example, we are modelling a dwarf signal. The zstore command creates a state space with a number variables, and invariants over the state, in a similar style to a Z schema. This functionality is provided by the session Z_Toolkit and Z_Machines.

The operations specify the ways in which we can update the state. They operate over a named state space, and make use of parameters that are drawn from a suitable set. The body of the operation specifies a number of preconditions, which must be satisfied to execute the operation. An update specifies the changes that are made to variables when the operation executes.

The next step is to show that each of the operations preserves the invariants. These invariants can be used to demonstrate that the model satisfies certain critical properties. We can use the zpog method to generate invariant proof obligations.

Using the Isabelle code generator, we can also animate Z Machines through a Haskell implementation. This allows us to step through the model's behaviour, for the purpose of prototyping.