Abstract: HOL-Z in the UniForM-Workbench ...

HOL-Z in the UniForM-Workbench -
a Case Study in Tool Integration for Z

C. Lüth1, Einar W. Karlsen1, Kolyang1, S. Westmeier1, B. Wolff2

1Bremen Institute for Safe Systems, FB 3, Universität Bremen
2 Universität Freiburg, Institut für Informatik

The UniForM-Workbench is an open tool-integration environment providing type-safe communication, a toolkit for graphical user-interfaces, version management and configuration management.

We demonstrate how to integrate several tools for the Z specification language into the workbench, obtaining an instantiation of the workbench suited as a software development environment for Z. In the core of the setting, we use the encoding HOL-Z of Z into Isabelle as semantic foundation and for formal reasoning with Z specifications. In addition to this, external tools like editors and small utilities are integrated, showing the integration of both self-developed and externally developed tools.

The resulting prototype demonstrates the viability of our approach to combine public domain tools into a generic software development environment using a strongly typed functional language.


Christoph Lüth, 01.07.98