TAS and IsaWin are tools for formal
program development and theorem proving developed at the University of
Bremen and Albert-Ludwigs-Universität, Freiburg.
TAS is a transformation system based on the theorem
prover Isabelle. It features:
transformations based on Isabelle theorems;
a graphical user
interface based on the principle of direct manipulation;
genericity (suitability for a whole range of formal methods).
In particular, genericity means it can be used for any formal
method which offers a notion of correctness-preserving refinement, or
in fact any transitive-reflexive transformation relation, which is
encoded into Isabelle. We have investigated instantiations for
classical program transformations (in the style of systems like KIDS
using plain higher-order logic), for the specification language Z
(using the HOL-Z
encoding), the process calculus CSP (using the HOL-CSP
encoding), and the algebraic specification language CASL (using
the HOL-CASL encoding).
IsaWin is a graphical user interface for the theorem
prover Isabelle. It offers the user a more abstract view on Isabelle
then its ususal command-line based interface.
Both systems are built using sml_tk,
an encapsulation of the user interface description language and
library Tcl/Tk into Standard ML (SML). Building on this, we provide a
Generic Interface Toolkit which can be used to quickly built graphical
user interfaces like TAS and IsaWin.
Demos and Screenshots
Here is a full screenshot of TAS and
IsaWin, but you to get a taste of TAS and IsaWin you can download a
demo version below. Note that these are preliminary
demo versions with a deliberately limited functionality.
The demos are plug&play without a complicated configuration
procedure. To run them, unpack the file tas_demo.tar.gz. This
will produce a directory tas_demo. Go into this directory,
and call bin/TAS_demo. The file README (in
tas_demo) contains further information.
TAS and IsaWin are still in a prototypical stage, so we unfortunately
at this point we can only make the demo versions above available to
the public. A full working version should be available by the start of
the next year.
Papers and Documentation
Here are a couple of papers about TAS and IsaWin. More can be found here and here.
C. Lüth, H. Tej, B. Wolff: Generic Transformational
Program Development. [PostScript] A general
explanation of TAS, its implementation and its user interface. It
should be read in conjunction with the demo (hence it is also included
there).
C. Lüth, B. Wolff: Functional Design and Implementation
of Graphical User Interfaces for Theorem Provers. Journal of Functional
Programming, 9(2): 167- 189, March 1999 [Abstract]
[PostScript]
This paper provides an in-depth explanation of the technology used to
implement TAS and IsaWin.
On a more historic note, the system YATS, the ancestor of TAS from
which it inherits its design and many concepts, is described in:
Kolyang, T.Santen, B. Wolff: Correct and User-Friendly
Implementations of Transformation Systems. Formal Methods Europe
1996, Oxford. Springer LNCS 1051, 1996. [Abstract],
[Postscript].
Personnel
TAS, IsaWin and the Generic Interface Toolkit are developed jointly by
Christoph Lüth at the University of Bremen and Burkhart Wolff
at the Albert-Ludwigs-Universität Freiburg. The development was
initially funded by the UniForM project.
Christoph Lüth.
Last modified: Tue Dec 2 16:09:09 CET 2003
