ccslc, ccslc.opt - The CCSL Compiler
ccslc [options ...] files ...
ccslc.opt [options ...] files ...
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.
Place all generated files in directory dir
Set the target theorem prover to PVS. This is the default.
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.
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.
Generate a batch processing file. The precise behaviour depends on the output mode.
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
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.
Only generate output for specification spec. Repeat this option to get output for several classes.
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.
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:
All type constructors in ground signatures must have arity zero.
All data types and all class specifications must be strictly covariant (i.e., all type parameters must have stricly positive variance).
No loose semantics for class specifications (i.e., Keyword FINAL is required.)
Assertions and creation conditions must be invariant with respect to behavioural equality. For this the compiler checks a sufficient condition that requires the following restrictions to the logic of CCSL:
polymorphic functions or constants (coming from ground signatures or preceding specifications) can only be instanciated with constant types
no function update (function update for functions with constant domain would be ok, but this is currently not implemented)
Equality over Self
Quantification over Self
-pedantic is mutually exclusive with -expert and -no-opt.
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.
Generate output for inductive characterization of invariants. This is currently experimental and does not work for all class signatures.
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.
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
Turn off inlining of liftings of the finite and infinite powerset type. Use the appropriate combinators instead.
Print the prelude to stdout. See also PRELUDE below.
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.
Backward compatibility. Use prelude from version 2.2. Back then
lift was called Lift and had a constructor bot instead
of bottom.
Print usage information.
Act as filter. Print all generated output to stdout.
Proofs only. Do not generate any theories, only generate proofs. Useful for proof testing.
Proof testing. Do not generate any output. Only print the proof for lemma name to stdout.
Verbose. Print some messages about compilation progress.
Set debugging flags to number. If several optinos -D are given the result is xor of numbers.
The compiler recognizes the following flags:
Verbose. Equivalent to -v.
Debug messages for the lexer.
Debug messages for the parser.
Debug messages for resolution pass.
Debug messages for inheritance pass.
Debug messages for type checking.
This value is no longer used.
Dump symbol table to stderr on unknown identifier.
Apply debugging level also when processing the prelude.
Debug messages for type unification
Print assertions, creation conditions, and theorems to stderr after parsing. Useful for problems with operator precedence.
Debug messages for variance pass.
Debug messages for feature pass.
Debug messages for pedantic checks.
This option is only present for backward compatibility. It has no effect.
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.
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
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>.
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.
CCSL at http://www.askra.de/ccsl/ , the LOOP project, PVS at http://pvs.csl.sri.com/ , Isabelle at http://isabelle.in.tum.de/ .
Hendrik Tews <hendrik@askra.de>, http://askra.de