The UniForM Workbench

The UniForM Workbench is a tool integration framework which allows users to develop formal software development environments based on the off-the-shelf development tools available, such as theorem provers or model checkers. The constituent parts of the workbench, such as HTk, can be used independently as well.

On this page, you can find:

A short description of the workbench and its parts.
Software and documentation.
Other Haskell documentation.

A Short Introduction to the UniForM Workbench

The UniForM workbench is written entirely in the functional programming language Haskell. It uses Haskell, extended with a higher-order model of concurrency, as a typed integration language (GlueWare). This extension forms the concurreny toolkit.

The integrated software development environment is modelled as a reactive system, with events as the primitive notion. Events can come from

the user, for example via a mouse click;
a tool;
other parts of the workbench.

These primitive events can in turn be combined and sequenced in various ways, to make more complicated events.

The subsystem interaction manager is a toolkit to encapsulate foreign tools. Its most important component is Haskell-Expect, which allows the easy encapsulation of tools with a text-based interface. The idea is to create events from regular expressions. Such an event is triggered when the tool outputs a string matching the corresponding regular expression. These events can then be combined and sequenced to allow arbitrarily complex dynamically-changing interactions between one or more tools and other parts of UniForM. Thus Haskell-Expect goes far beyond the original Unix expect program, which inspired it.

To allow the development of state-of-the-art graphical user interfaces in a functional style, the workbench provides HTk, an encapsulation of Tcl/Tk, which is based on Haskell-Expect. It combines the advantages of Tk (platform independency, abstraction) with the advantages of Haskell (type safety), bypassing the shortcomings of Tcl (untypedness, lack of structuring concepts).

In HTk, widgets are modelled as datatypes, and the different configuration options as type classes, allowing many errors which in Tcl/Tk only occur at runtime to be caught by typechecking. User inputs are modelled by events, to which the system reacts asynchronously, making HTk fully concurrent.

Obtaining the Workbench

A tarball of the latest release of the workbench will be availble here shortly. For the time being, to obtain the very latest version of the workbench, use our public CVS server - here's how to use it.

To compile the workbench, you need the Glasgow Haskell Compiler Version 5.02 - download it from here.

We have compiled and tested the workbench under Linux i86 and Solaris Sparc systems. Other architectures, if supported by the Glasgow Haskell Compiler (GHC), may work, but are untested due to lack of availability. You will probably need around 150MB of disk space and 128MB of main memory.

Documentation and Papers

The most comprehensive description of the workbench and its design philosophy is Einar Karlsen's doctoral dissertation, Tool Integration in Functional Programming Language (Universität Bremen, 1998). It has by now been obsoleted by ongoing development, but still describes the main design ideas.

Personell and Contact Info

The UniForM workbench was originally conceived and developed by Einar Karlsen. Currently, it is being maintained and developed further by George Russell and Christoph Lüth.

If you have any questions or feedback at all, please drop us a mail at uniform@informatik.uni-bremen.de.

Last modified: Fri Feb 8 14:59:15 MET 2002