| | | Tools |
The aims of this task group are threefold:
The Casl tool set (CATS, [37]) is an integrated set of tools combining a parser, a static checker, a LaTeX pretty printer and facilities for printing signatures of specifications and structure graphs of Casl specifications, with links to various verification and development systems. In addition, we plan to provide a structure editor, an Emacs mode, and a graphical interface to display the structure graphs. To experiment with Casl specifications, the CATS system provides different user interfaces: a Web-based interface, and a compact stand-alone version. A repository with successfully and unsuccessfully parsed specifications is under development.
Casl offers a flexible syntax including mixfix notation, which requires advanced parsing technology. ASF+SDF was used to prototype the Casl syntax in the course of its design, and several other parsers have been developed concurrently with the concrete syntax, which had the advantage of helping to detect ambiguities and inconsistencies in the syntax, cf. [7], [53], [39].
A LaTeX package for formatting Casl specifications has been developed [44]. This package is aimed at facilitating the pretty-printing and the uniform formatting of Casl specifications, and the easy combination of parts of documents written by different authors. An automatic conversion from LaTeX to HTML provides another widely available format for exchanging specifications through the Web.
Interoperability of Casl and existing tools is a major goal of the Tools group. The first step has been to propose an interchange (or interoperability) format that can be accepted as input and output by every tool. The starting idea was to adopt basically abstract syntax trees with annotations providing specific information to communicate with various tools (parsers, rewrite engines, proof tools, etc.). The Annotated Term (ATerm) Format described in [8] has been chosen as a common interchange format for CoFI tools. Work is in progress to also provide XML as an external interchange format. Based on either of these low-level formats, several high-level formats such as CasFix [9] (for abstract syntax trees of Casl specifications), CasEnv (for global environments containing signature information etc.) and FCasEnv (a flattened version of CasEnv, for use with tools that do not support structured specifications) have been developed. Formats for storing proofs and developments will follow.
Existing rewrite engines embedded in OBJ, ASF+SDF and ELAN provide a good basis for prototyping (parts of) Casl specifications. For instance, the ELAN compiler [31] efficiently supports many-sorted conditional rewrite rules with associative commutative functions. A first prototype has been realised that reads in the FCasEnv format, and translates it into EFix format (ATerms for ELAN) which can then be executed by the ELAN interpreter or compiled to produce C code [27].
The standalone version of CATS also contains an encoding into several other logics. The encoding transforms a Casl specification into second-order logic step by step. First, partiality is encoded via error elements living in a supersort; second, subsorting is encoded via injections; and third, sort generation constraints are expressed via second-order induction axioms. It is possible to stop after the first or second step if one wants to use a tool supporting subsorting or sort generation constraints directly. For details, see [36], where alternative encodings are also described. In this way, CATS allows to interface Casl with a large number of first- and higher-order theorem provers.
The HOL-CASL system, being built on top of CATS, uses the encoding of Casl into second-order logic to connect Casl to the Isabelle theorem prover and the generic graphical user interface IsaWin. This approach to encoding Casl in proof systems such as Isabelle or PVS allows verification and program transformation [39][36].
Various verification tools have already been developed for algebraic specifications, and can be reused for specific subsets of Casl: equational, conditional, full first-order logic with total functions, total functions with subsorts, partial functions, etc. The system INKA 5.0 [3] provides an integrated specification and theorem proving environment for a sub-language of Casl that excludes partial functions (with the encoding provided by CATS, it will also be useable with full Casl); a similar adaptation of the KIV [47] system is under way.
Currently, CATS is connected to the development graph management component of the INKA theorem proving system [3]. Structured Casl specifications in the CasEnv format are translated to development graphs [4]. The development graph supports the management of theories and proof obligations that arise from Casl specifications in a theorem prover-independent way. Moreover, it provides an efficient way of managing change, allowing re-use of those parts of proofs that are not affected by the change of a specification.
The next step is the integration of other existing tools, especially for prototyping and verification. Participants of the Tools group already have experience with tool integration, with Corba-IDL [26], the Tool Bus [5] developed in Amsterdam, and the UniForM Workbench [29] developed in Bremen.
All tools developed in the CoFI Tools group are made available to the community, after validation by the Tools group. A Web page for tools [18] describes on-going work and interests, giving access to available tools, and giving guidelines on how to propose a new tool.
| | | Tools |