This directory contains the CCSL compiler version 2.2.6.

For installation instructions see file INSTALL in this directory.

This file contains general information about CCSL and the CCSL
compiler. 

#####################################################################
# $Id: README.in,v 1.2 2003/08/21 15:15:11 tews Exp $
#####################################################################


OVERVIEW

CCSL stands for Coalgebraic Class Specification Language. It 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 Isabelle/HOL. After
translation the theorem prover can be used to examine the
specification, built models, construct refinements, and much more.

The PVS back end has been tested and is considered to be complete.
The Isabelle back end (in new style Isar syntax) works but with
our test cases. However, the Isabelle back end has not been
tested in a case study.

CCSL has been developed in the LOOP project, for more information
about the LOOP project, see http://www.cs.kun.nl/~bart/LOOP/.



DOCUMENTATION

The interface of the CCSL compiler is described in its man page,
see Doc/ccslc.1 or wherever it was installed.

Apart from that there is not much documentation, sorry about that. 

The subdirectory doc/ contains the grammar of CCSL, see
grammar.{txt,html}. 

CCSL is described (and used) in some papers. These papers are
linked on the CCSL home page
(http://wwwtcs.inf.tu-dresden.de/~tews/ccsl/).

- general introduction into CCSL:

  J. Rothe, H. Tews, B. Jacobs, The Coalgebraic Class
  Specification Language CCSL. Journal of Universal Computer
  Science 7(2):175-193.


- coalgebraic refinement with a large CCSL example

  B. Jacobs, H. Tews, Assertional and Behavioural Refinement in
  Coalgebraic Specification. 


- complete syntax and semantics of CCSL, see Chapter 4 of

  H. Tews, Coalgebraic Methods for Object-Oriented Specification.
  Draft PhD thesis. Available at
  http://wwwtcs.inf.tu-dresden.de/~tews/PhD/. 




CONTENTS

Ccsl/		\
Common/		 >  compiler sources
Keywords/	/
Doc/		some documentation
README		this file
INSTALL		installation instructions
COPYING		the license



BUGS / PROBLEMS / CONTACT

If you encounter problems during installation or have questions
about CCSL then please contact me at tews@tcs.inf.tu-dresden.de.


-----------------------------------------------------------------
Hendrik Tews     Department of Theoretical Computer Science
                 Dresden University of Technology, Germany

Telefon:   	 +49 351 463 38351
e-mail:    	 tews@tcs.inf.tu-dresden.de
www:       	 http://home.pages.de/~tews/
pgp key:         http://home.pages.de/~tews/pgpkey.asc
-----------------------------------------------------------------


**********************************************************************
** This program is free software; you can redistribute it and/or
** modify it under the terms of the GNU General Public License as
** published by the Free Software Foundation; either version 2 of
** the License, or (at your option) any later version.
** 									      
** This program is distributed in the hope that it will be useful,
** but WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
** General Public License in file COPYING in this or one of the
** parent directories for more details.
**********************************************************************

*** Local Variables: ***
*** mode: text ***
*** version-control: t ***
*** kept-new-versions: 5 ***
*** delete-old-versions: t ***
*** End: ***