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.

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.

The latest (in the meantime outdated) release is version 2.2.6. Download ccsl.tar.gz. Older releases are here.

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 2up ps.gz] [a4 2up ps] [a4 ps.gz] [a4 ps] [a4 dvi] [a4 pdf]
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 2up ps] [a4 ps.gz] [a4 ps] [a4 dvi] [a4 pdf] [letter 2up ps.gz] [letter 2up ps] [letter ps.gz] [letter ps] [letter dvi] [letter pdf]

• 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] [full-paper.ps] [extended-abstract.ps.gz] [extended-abstract.ps]

• 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] [a4.ps] [everything.tar.gz] [everything.tar]

Anonymous CVS Access

For users who are interested in more frequent updates and the latest development I recomment to install CCSL via remote cvs.

To connect to the CCSL repository for the first time do the following:

1. Login into the remote CVS server:

   cvs -d :pserver:guest@tcs.inf.tu-dresden.de:/usr/local/cvs-ccsl login
          

   (The whole command should be on one line.)

   You will be prompted for a password, which is ``guest''.

   With some cvs versions this command fails with something like "cvs login: failed to open /home/itt/tews/.cvspass for reading ...". In this case create the the file ~/.cvspass manually with

   touch ~/.cvspass
          

   and try again.

2. Check out the CCSL module:

   cvs -d :pserver:guest@tcs.inf.tu-dresden.de:/usr/local/cvs-ccsl co -r latest-stable Ccslc
         

   (Again, type this on one line. latest-stable is the cvs tag for the latest stable version. )

   If this command fails with "cvs checkout: authorization failed: .... try "cvs login" with a real password", then your cvs version probably wrote a wrong entry into ~/.cvspass. Retry step one (without deleting ~/.cvspass) until ~/.cvspass contains a line like

   :pserver:guest@tcs.inf.tu-dresden.de:/usr/local/cvs-ccsl AIbdZ,
          

3. [NOT recommended] If you want to work with the CCSL test cases then you also have to check out the Ccsl_Testcases module:

   cvs -d :pserver:guest@tcs.inf.tu-dresden.de:/usr/local/cvs-ccsl co -r latest-stable Ccsl_Testcass
         

4. To update to the newest version, do

   cvs update
          

   from time to time in the new directories. This works because I change the latest-stable tag whenever I finished some task.

5. Optionally, log out of the server after use:

   cvs -d :pserver:guest@tcs.inf.tu-dresden.de:/usr/local/cvs-ccsl logout
         

   (Again, type this on one line.)

6. Change to the Ccslc directory created in step 2

   cd Ccslc
         

   and proceed with step 2 from file INSTALL.

Future Plans

• Allow modal operators of the current class in definitional extensions
• Past time modal operators Once, Previously
• add mu-calculus-like fixed point formulas
• support for monads and monadic actions for specifying side effects
• More syntactic sugar: elseif

In the long term CCSL will be enriched with generic algebraic specifications. Currently we disscuss syntax and intentional semantics of this extension on this page.

Contact

If you have specific questions you can also contact me at tews@tcs.inf.tu-dresden.de.

Links

• The LOOP project on formal methods of object orientation.
• Back to my home page.