Abstract: CCC - The CASL Consistency Checker

CCC - The CASL Consistency Checker

Christoph Lüth
FB 3 - Mathematik und Informatik, Universität Bremen

Markus Roggenbach
Department of Computer Science, University of Wales Swansea

Lutz Schröder
FB 3 - Mathematik und Informatik, Universität Bremen

We introduce the CASL Consistency Checker (CCC), a tool that supports consistency proofs in the algebraic specification language CASL. CCC is a faithful implementation of a previously described consistency calculus. Its system architecture combines flexibility with correctness ensured by encapsulation in a type system. CCC offers tactics, tactical combinators, forward and backward proof, and a number of specialised static checkers, as well as a connection to the CASL proof tool HOL-CASL to discharge proof obligations. We demonstrate the viability of CCC by an extended example taken from the CASL standard library of basic datatypes.


Christoph Lüth, 05.10.04