We provide several user interfaces to the Bremen HOL-CASL system. Actually, it has turned out that for the first contact with our tool, the most important user interface is the web-based interface4, where the user can just type in a specification, and parse it, perform the static analysis and/or conversion to LaTeX. Most users want to try out this easy-to-use interface before taking the effort to download the stand-alone version (even if the latter effort is very small). The web-interface has even been used as a front-end in a prototype translation to PVS [Bai99] (although it is much more convenient to use the stand-alone version in this case).
Figure 5: The HOL-CASL instantiation of the IsaWin system
The small stand-alone version of our tool5 provides the full functionality shown in Fig. 2, except the Isabelle theorem proving environment. It has been quite crucial to exclude Isabelle here, since Isabelle is quite large, and users who want to use the tool as a front-end or back-end do not want to download the whole Isabelle system. The stand-alone tool can be called as a Unix command, and the different entry points and phases of analysis and encodings of the tool (cf. Fig. 2) can be selected with optional flags. In particular, it is also possible to select the encoding into FOL/HOL without having to use Isabelle (this is useful when combining our tool with theorem provers for first- or higher-order logic). We also plan to make the different steps of the encoding (see section 6) separately available, so that one can choose to "encode out" just partiality and keep the subsorting (this will be useful, for example, in connection with Maude [CDE+99] which supports subsorting). The Unix interface works quite well when using the tool in combination with other tools, although we plan to provide a fully-fledged applications programmer interface (API) in the future.
The full stand-alone version of the tool6 also provides the Isabelle theorem prover, and the generic graphical user interface IsaWin [LW99, LTKKB99], which has been built on top of Isabelle. We have instantiated IsaWin with our HOL-CASL encoding of CASL into Isabelle/HOL. In Fig. 5, you can see a typical IsaWin window. The icons labelled with (Sigma,E) are CASL specifications (more precisely, their encodings in HOL). Note that HOL itself also is available at this level. The icon labelled with a tree is an open proof goal. By double-clicking on it, you can perform proof steps with this goal. This is done by dragging either already proven theorems (those icons marked with |- A) or simplifier sets (icons marked with {l -> r}) onto the goal. The effect is the resolution of the goal with the theorem thrown onto it, or the rewriting of the goal with the chosen simplifier set. After the proof of a goal is finished, it turns into a theorem. You can then use it in the proof of other theorems, or, if it has the form of a rewrite rule, add it to a simplifier set.
Actually, some users explicitly told us that they feared to have to install Isabelle to run our tool, but even the full version including Isabelle and IsaWin is completely stand-alone (apart from the need to install Tcl/Tk, which has already been installed on many sites).
