CCSL site navigation:
CCSL home page
Legacy Version 3 Discussion
CCSL - The Coalgebraic Class Specification Language
Welcome to the Website of CCSL. CCSL has been developed between
1997 and 2004. Although development has ceased since then the
compiler is still fully functional.
CCSL is a
specification language that combines both algebraic and coalgebraic
elements. The CCSL compiler translates CCSL specifications into
higher-order logic either for
for Isabelle/HOL (in new
style Isar syntax).
translation the theorem prover can be used to examine the
specification, built models, construct refinements, and much more.
The specification language CCSL contains the following elements:
- single sorted, parametric coalgebraic specifications with the
- coalgebraic signatures correspond to higher-order polynomial
functors, that is to polynomial functors with arbitrary
exponents. This gives direct support for binary methods and
method types with functional arguments.
- the class of models is restricted with axioms in higher-order
- the logic is extended with behavioural equality and method
wise infinitary modal operators
- additional operations can be defined as definitional
- support for final and loose semantics
- inheritance of specification allows one to (monotonically)
- record-like state space is supported with automatic
generation of update methods and axioms for these
- constructors capture operations for object creation
- single sorted, parametric algebraic abstract data types (as
they are found in PVS and Isabelle). Formulated the other way
round: algebraic specifications without axioms and with initial
- signature extensions with type constructors and arbitrary
The PVS back end of the CCSL compiler
has been tested and is considered to be complete.
The Isabelle back end works with our testcases but has not been
used in a case study.
CCSL has been developed within the LOOP project (whose website
has disappeared). Nowadays CCSL has similarities with CoCasl, but at the time CCSL has been developed, CoCasl did
not exist yet.
Get and run CCSL
The CCSL compiler is distributed as source code under the GNU
General Public License.
You can download the most recent snapshot as ccsl.tar.gz.
Older releases are available in the download directory.
For installation instructions see the file INSTALL.
See the file
for general information.
To compile the CCSL compiler you need a recent version of Ocaml. The CCSL compiler
should run on any platform supported by Ocaml (I actually tested
Debian Linux and SunOS).
To make use of CCSL you need a theorem prover for higher-order
logic. I highly recomment installing PVS.
The following documentation is available:
CCSL is also described (and used) in some papers.
- CCSL Tutorial, DRAFT Version
- The tutorial is in a very early state, it only covers the
construction of models in PVS at the moment.
The examples used in the tutorial are available as compressed tar
- CCSL Reference Manual
- Unfortunately the reference manual is currently in a state
that cannot be distributed.
- Compiler man page
- describing the command line interface of the CCSL compiler:
ccslc man page.
- The distribution contains the grammar of CCSL in BNF as text and
as html file. The html version can also be
- The complete syntax and semantics of CCSL is described in
full technical glory in the technical report The Coalgebraic
Class Specification Language CCSL -Syntax and Semantics.
The report is (almost) identical with Chapter 4 of my PhD.
[a4 2up ps.gz]
For questions about CCSL please email
last modified on
20 Sep 2011