Casl Tools

Casl Tools

See the Tools activity pages for a more detailed and up-to-date description of the available Casl tools.

Integated Casl Tool Set:

The Casl Tool Set, CATS, 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.

To experiment with Casl specifications, the CATS system provides different user interfaces: a Web-based interface, and a compact stand-alone version.

Formatting Casl Specifications:

A LaTeX package for formatting Casl specifications has been developed [44]. Marked-up Casl specifications can be formatted in DVI and PostScript, and as hypertext documents in HTML and PDF.

Interchange Format:

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.

Translation to other logics:

The standalone version of CATS also contains an encoding into several other logics. In this way, CATS allows to interface Casl with a large number of first- and higher-order theorem provers.

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.

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.

Please contact the CoFI Tools Task Group Coordinator if interested in participating in this work!

Casl Tools