Abstract:

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

Chritoph Lüth and Einar W. Karlsen and Kolyang and Stefan Westmeier and Burkhart Wolff


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.


doi:10.1007/BFb0056029
http://www.springerlink.com/content/w266638271586141/