NAME

ccslc, ccslc.opt - The CCSL Compiler


SYNOPSIS

ccslc [options ...] files ...

ccslc.opt [options ...] files ...


DESCRIPTION

ccslc compiles CCSL specifications in the argument files into higher-order logic for either PVS or Isabelle/HOL.

ccslc.opt is the optimized version of ccslc. It is available if this platform supports the ocaml native code compiler.

The normal behaviour of the compiler is as follows. It reads and type checks CCSL specifications from the input files and computes their semantics in higher-order logic (HOL). The semantics is taken with respect to a basic environment, resulting from processing the prelude (see PRELUDE below). Every input file defines its own name space. That is, specifications in file file1 are not visible in file2. At the end the compiler outputs the semantics of the specification in the syntax of the target theorem prover.

The compiler supports two target theorem provers: PVS and Isabelle/HOL. The default is to generate output for PVS.


OPTIONS

-d dir

Place all generated files in directory dir

-pvs

Set the target theorem prover to PVS. This is the default.

-isa

Set the target theorem prover to Isabelle/HOL (new style Isar syntax). Of a sequence of -pvs and -isa options the last one takes effect.

-nattype type

Set the type name of natural numbers to type. Defaults to nat. More precisely, the type checker uses type type for all natural number constants (consisting only of digits) in the source. This option is necessary to prevent type checking errors if you use natural number constants in combination with a type different from nat.

Note that type must be a valid type at each occurance of a natural number constant in the source. So you probably need to add a ground type declaration for type at the start of the specification.

-batch

Generate a batch processing file. The precise behaviour depends on the output mode.

PVS:

Generate a file pvs-batch.el in the target directory. This file contains Emacs lisp code and causes PVS to type check all files in the right order when evaluated. Process this file in PVS with M-x load-file pvs-batch.el

Isabelle/HOL:

Generate a file ROOT.ML in the target directory. This file contains Isabelle SML code for loading all relevant files. The isabelle option -u causes Isabelle to automatically load ROOT.ML.

-class spec

Only generate output for specification spec. Repeat this option to get output for several classes.

-dependent-assertions

Normally the semantics of an assertion is a predicate on the state space that is independent from all other assertions. With this option each assertions has the preceeding assertion as assumption. This does not change the semantics of a class specification. However, it makes it possible to discharge type-check conditions (TCC's) with the help of previous assertions.

-pedantic

Very strict input checking to avoid consitency problems. This option restricts CCSL to the iterated functors from Martin Roessigers PhD thesis. His theorems ensure the existence of initial models of data types and final models of class specifications (as long as your assertions are consistent). -pedantic enforces the following restrictions:

-pedantic is mutually exclusive with -expert and -no-opt.

-expert

Turn on expert mode. This turns a number of errors into warnings. As a result the compiler might generate inconsistent output. For obvious reasons -expert cannot be used with -pedantic.

-path

Generate output for inductive characterization of invariants. This is currently experimental and does not work for all class signatures.

-no-opt

Turn off formula optimization. Normally the CCSL compiler performs several optimizations before printing formulas and expressions. With this option the generated output is nearly unreadable. This option cannot be used with -pedantic to ensure that equality is used as relation lifting on constant types.

-no-inline-lifting

Turn off the inlining of liftings of non-recursive classes and of abstract data types. A non-recursive class (abstract data type) is one whoose signature corresponds to a constant functor. The predicate and relation lifting for such classes is a conjuntion; and for non-recursive abstract data types it is a case distinction. Normally the CCSL compiler uses these liftings directly. With the option -no-inline-lifting it uses the appropriate combinators instead. To turn off the inlining of powerset liftings use -no-inline-power-lifting

-no-inline-power-lifting

Turn off inlining of liftings of the finite and infinite powerset type. Use the appropriate combinators instead.

-output-prelude

Print the prelude to stdout. See also PRELUDE below.

-no-prelude

Do not magically prepend the prelude to the first input file. That is, all input files are processed in a vanilla ground signature. For method-wise modal operators the compiler needs the type constructor for lists. Therefore the compiler aborts if one input file does not define a type constructor list. If the type constructor is defined with a different semantics strange things will happen.

-old-lift

Backward compatibility. Use prelude from version 2.2. Back then lift was called Lift and had a constructor bot instead of bottom.

-help
--help

Print usage information.

-c

Act as filter. Print all generated output to stdout.

-prf

Proofs only. Do not generate any theories, only generate proofs. Useful for proof testing.

-prooftest name

Proof testing. Do not generate any output. Only print the proof for lemma name to stdout.

-v

Verbose. Print some messages about compilation progress.

-D number

Set debugging flags to number. If several optinos -D are given the result is xor of numbers.

The compiler recognizes the following flags:

-D 1

Verbose. Equivalent to -v.

-D 2

Debug messages for the lexer.

-D 4

Debug messages for the parser.

-D 8

Debug messages for resolution pass.

-D 16

Debug messages for inheritance pass.

-D 32

Debug messages for type checking.

-D 64

This value is no longer used.

-D 128

Dump symbol table to stderr on unknown identifier.

-D 256

Apply debugging level also when processing the prelude.

-D 512

Debug messages for type unification

-D 1024

Print assertions, creation conditions, and theorems to stderr after parsing. Useful for problems with operator precedence.

-D 2048

Debug messages for variance pass.

-D 4096

Debug messages for feature pass.

-D 8192

Debug messages for pedantic checks.

-fixedpointlib path

This option is only present for backward compatibility. It has no effect.


DIAGNOSTICS

Error reporting is relatively poor. The compiler reports only the first error it finds in one source file. It then continues processing the next source file.


PRELUDE

The prelude consists of some CCSL specifications that are magically read before the first file, making types and constants available for the specifications. The prelude is hard-wired into the compiler and it depends on the target theorem prover. The prelude refers to some nonstandard theories, like EmptyTypeDef. Those theories are magically created when the prelude is read.

For PVS the prelude is:

   Begin EmptySig : GroundSignature
      Importing EmptyTypeDef
      Type EmptyType
   End EmptySig
   Begin EmptyFunSig [A : Type]: GroundSignature
      Importing EmptyFun[A]
      Constant
         empty_fun : [EmptyType -> A];
   End EmptyFunSig
   Begin list[ X : Type ] : Adt
      Constructor
         null : Carrier;
         cons( car, cdr ) : [X, Carrier] -> Carrier
   End list
   Begin lift[ X : Type ] : Adt
      Constructor
         bottom : Carrier;
         up( down ) : X -> Carrier
   End lift
   Begin Coproduct[ X : Type, Y : Type ] : Adt
      Constructor
         in1(out1) : X -> Carrier;
         in2(out2) : Y -> Carrier;
   End Coproduct
   Begin Unit : Adt
      Constructor
         unit : Carrier;
   End Unit
   Begin PowerSig[X : Pos Type] : Groundsignature
     Importing PowerDefs2
     Type Power
     Constant
       emptyset : Power[X];
       member : [X, Power[X]] -> bool;
       pred : Power[X] -> [X -> bool]
   End PowerSig
   Begin FPowerSig[X : (?,0) Type] : Groundsignature
     Importing FPowerDefs2
     Type FPower
     Constant
       femptyset : FPower[X];
       fmember : [X, FPower[X]] -> bool;
       fpred : FPower[X] -> [X -> bool]
   End FPowerSig

In Isabelle/HOL there is no empty type and the lists are slightly different. So the Isabelle/HOL prelude is

   Begin list[ X : Type ] : Adt
      Constructor
         Nil : Carrier;
         Cons( car, cdr ) : [X, Carrier] -> Carrier
   End list
   Begin lift[ X : Type ] : Adt
      Constructor
         bottom : Carrier;
         up( down ) : X -> Carrier
   End lift
   Begin Coproduct[ X : Type, Y : Type ] : Adt
      Constructor
         in1(out1) : X -> Carrier;
         in2(out2) : Y -> Carrier;
   End Coproduct
   Begin Unit : Adt
      Constructor
         unit : Carrier;
   End Unit
   Begin PowerSig[X : Pos Type] : Groundsignature
     Type Power
     Constant
       empty : Power[X];
       member : [X, Power[X]] -> bool;
       pred : Power[X] -> [X -> bool]
   End PowerSig


BUGS

The compiler is research software, draw your own conclusions about the presence of bugs.

Internal compiler errors are reported like this:

    Error: Assertion in file: t.beh (pvs_mode)
    See class_theorems_theory.ml, char 2378-2391

Please report all errors and bugs to <ccsl@askra.de>.


CREDITS

CCSL has been developed within the LOOP project on formal methods for object-orientation (the LOOP website disappeared).

Many people contributed to the source code, including Ulrich Hensel, Bart Jacobs, Rothe Jan, Wim Jansen, Huisman Marieke, Hendrik Tews, and Joachim van den Berg.


SEE ALSO

CCSL at http://www.askra.de/ccsl/ , the LOOP project, PVS at http://pvs.csl.sri.com/ , Isabelle at http://isabelle.in.tum.de/ .


AUTHOR

Hendrik Tews <hendrik@askra.de>, http://askra.de