CCSL site navigation: CCSL home page Legacy Version 3 Discussion

CCSL - The Coalgebraic Class Specification Language

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:

• single sorted, parametric coalgebraic specifications with the following elements:
  • 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 logic
  • the logic is extended with behavioural equality and method wise infinitary modal operators
  • additional operations can be defined as definitional extensions
  • support for final and loose semantics
  • inheritance of specification allows one to (monotonically) extend specifications
  • record-like state space is supported with automatic generation of update methods and axioms for these update methods
  • 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 semantics.
• signature extensions with type constructors and arbitrary (polymorphic) constants.

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

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

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]

• For a general introduction and presentation of CCSL see

  Jan Rothe, Bart Jacobs, and Hendrik Tews, The Coalgebraic Class Specification Language CCSL. Journal of Universal Computer Science 7(2):175-193.
  copy [full-paper.ps.gz] [extended-abstract.ps.gz]

• For coalgebraic refinement and a refinement example in CCSL see

  Bart Jacobs and Hendrik Tews, Assertional and Behavioural Refinement in Coalgebraic Specification
  Section 6 of this paper contains a small case study on a transaction-commit mechanism in CCSL. The source code is available at this page.
  copy [a4.ps.gz]

Contact

Home Science Overview All Publications Talks PhD CCSL Robin