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 PVS or for for Isabelle/HOL (in new style Isar syntax). After 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:

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 README 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.

Documentation

The following documentation is available:

CCSL Tutorial, DRAFT Version
The tutorial is in a very early state, it only covers the construction of models in PVS at the moment.
copy [a4 ps.gz]
The examples used in the tutorial are available as compressed tar file: [download stack.tar.gz]
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.
Grammar
The distribution contains the grammar of CCSL in BNF as text and as html file. The html version can also be viewed online.
Semantics
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.
copy [a4 2up ps.gz] [a4 ps.gz]

CCSL is also described (and used) in some papers.

Contact

For questions about CCSL please email ccsl@askra.de.


Home Science Overview All Publications Talks PhD CCSL Robin


last modified on 20 Sep 2011 by Hendrik