CCC – The Casl Consistency Checker
Christoph Lüth, Markus Roggenbach, Lutz Schröder · Lecture notes in computer science · 2005
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.