Introduction
CCC, the CASL Consistency Checker, is a tool to prove the
consistency of specifications written in the algebraic
specification language CASL (see the
CoFI pages for
further information concerning this language), i.e. to show that
the specification has at least one model.
The CCC is based on a calculus presented here. Its strategy for consistency proofs is as
follows: guided by the structure of the specifiation text, one
splits up the original proof goal by applying certain proof
rules into simpler properties, avoiding the need to construct
(and prove) actual models of specifications as far as
possible.
CCC is a faithful implementation of this consistency calculus.
It is based on a logical core, representing the rules of the
calculus. On top of this core, a body of derived rules and
tactics is built. Moreover, CCC offers proof management and a
number of specialized static checkers, as well as a connection
to the CASL proof tool HOL-CASL which facilitates discharging
proof obligations.
Download
You can download CCC in various packages:
- Binary Package: ready-to-run binaries for Sparc-Solaris
and x86-Linux systems (warning: quite large).
- Source Package: (requires Isabelle99-2 and CATS to compile, but
quite small).
Instructions
After downloading, unpack CCC in a directory of your choice (all
tar archives will unpack into a directory called
ccc),
cd into that directory and do
./configure [options]
to configure CCC. Options are only needed if you want to
configure the source package, the binary version
does not need options (but it needs to be configured!):
- --with-cats=path
Sets the path to CATS.
- --with-isabelle=path
Sets the path to the Isabelle startup script isabelle
(which starts up Isabelle in the ML interface). Note
CCC (HOL-CASL, actually) needs Isabelle99-2, not the
newer Isabelle2002. The binary package comes with its
own copy of Isabelle99-2, so you can use that to
compile the sources as well.
To build CCC, cd to the directory
ccc/src, and do
./build [HOL-CASL | ttt | clean ]
You'll need
CATS and HOL-CASL, and
Isabelle 99-2 (see under download, past releases).
To run CCC, use
ccc/bin/ccc. See the file
ccc/INSTALL for further information.
The Files
Bibliography
A paper describing the foundations of CCC: