CCSL site navigation: CCSL home page Legacy Version 3 Discussion

Legacy page on CCSL Version 3

Around 2003 we made plans for various extensions of CCSL, most notably with full multi-sorted algebraic specifications. However, the development on CCSL ceased before any of these plans could be worked out or implemented. The suggestions on this page will probably never become real.

The extensions discussed on this page comprise

The description below refers to the current CCSL grammar and uses the same conventions as there.

General Specifications

Currently specifications are either abstract data types or coalgebraic class specifications. For abstract data types one has initial semantics, for class specifications one can choose between loose and final semantics. General specifications superseed all that.


    BEGIN identifier [ parameterlist ] COLON [ modifier ] SPEC 
       { section } 
    END identifier

The modifier fixes the semantic that is used for that specification. The modifiers FINAL and INITIAL place additional (not yet specified) constraints on the contents of the specification. An ommited modifier defaults to LOOSE.

The parameter list can contain theory parameters of the forms X : specid, where specid is some specification, see generic specification below.

As now a specification contains different sections, where each section starts with a descriptive keyword. Possible sections are



Open Problems


In CCSL 2.x the name of the specification is used as a type constructor. Further, inside the specification the keywords CARRIER or SELF refer to the type that is just defined. The sort section makes all that more flexible and prepares for multi-sorted specifications.


    SORT identifier { COMMA identifier }
Every sort identifier is a valid type inside the specification. The semantics of the specification defines a set for every sort identifier (or an indexed collection if the specification is parametric).

If the sort section is missing it defaults to one sort identifier, which is identical to the name of the specification.

In CCSL 2.x every specification defines a type constructor, where the arity of the type constructor corresponds to the number of type parameters. In CCSL 3 you get a type constructor for every sort identifier. All those type constructors have the same arity.

The semantics (i.e., INITAL/FINAL/LOOSE) applies to all sorts. So it is not possible to have a two-sorted specification, where one sort is loose and the other initial. Use type parameters for that case.

The case of multi-sorted specifications with final semantics has not been worked out. It is unclear if there are any examples that are not artificial.


The section for operations superseeds the following sections: METHOD, CONSTRUCTOR, and (in parts) ATTRIBUTE.


    OPERATION operation { SEMICOLON operation }

    identifier COLON type
  | identifier COLON type ARROW type
Every operation defines a term of that type. The semantics contains one function for every operation. For initial and final specifications there are the known restrictions for types. For loose specifications there are no restrictions.


The keywords METHOD, ATTRIBUTE, and CONSTRUCTOR are synonyms for OPERATION. In addition they place the restrictions on the types of the declared operations. For operations declared with ATTRIBUTE there are (implicitly generated) update operations with the obvious Axioms.

Open Problems


The section for axioms superseeds the sections for assertions and creation conditions. The syntax is the same as for creation conditions. One gets algebraic specifications by placing axioms in a specification with initial semantics.

Open Problems


Extensions allow one to built a subspecification hierarchy without textual copying.


    EXTENDING identifier [ argumentlist ] 
       { COMMA identifier [ argumentlist ] }
Extensions are considered as syntactical sugar: The contents of the named specification is instanciated and copied.

Open Problems


The renaming section superseeds the renaming clause in the inherit section. There is a separate section for renamings in CCSL 3 because one might want to rename identifiers from theory parameters (see generic specifications).


    RENAMING renaming { andorcomma renaming }

    identifier DOUBLECOLON idorinfix AS idorinfix

In a renaming spec::id AS newid the identifier spec refers to a theory parameter or to a specification that appears in an EXTENDING section. If newid has the from of an infix operator then the compiler checks if the type of spec::id is valid for infix operators.

Open Problems

Generic Specifications

In CCSL 3 a specification can be parametrised by an arbitrary other specification. This is achieved by allowing parameters of the form X : ospec or X : ospec[T], where ospec is the name of some other specification.


    OBRACKET parameters { COMMA parameters } CBRACKET

    identifier { COMMA identifier } COLON [ variance ] TYPE
  | identifier { COMMA identifier } COLON [ variance ] identifier [ argumentlist ]

A parameter declared with the keyword TYPE is called a type parameter. Other parameters are called theory parameters. The identifier in a theory parameter must refer to a specification. Semantically, theory parameters give rise to an indexing by models (instead of sets as for type parameters).

Identifiers from a theory parameters are available via the :: prefix: Assume a theory parameter X : ospec. Then X::id refers to id in ospec. Infix operators from spec can only be used as prefix operators in the form X::(+). One can use a renaming section to make items from ospec available without the X:: prefix. This way items from ospec can become infix operators (again).

Open Problems

Signature morphisms, Specification values, and Instanciations

To make use of generic specifications it is necessary to have expressions that evaluate to specifications and to instanciate generic specifications with such expressions.


    OBRACKET argument { COMMA argument } CBRACKET

  | theoryexpression

    identifier [ argumentlist ] [ RENAMING renaming ]
  | VIEW identifier [ argumentlist ] AS identifier [ RENAMING renaming ]
  | GENERATE identifier FROM identifier [ argumentlist ] [ RENAMING renaming ]

Arguments are positional: The first argument is used for the first parameter, the second argument for the second parameter and so on. Arguments and parameter must have the same kind. That is, a type parameter must be instanciated with type expressions and theory parameter must be instanciated with theory expressions.

Let G[T : Type, S : ospec] be a generic specification, where ospec is some specification without parameters. Then G[ nat, ospec] refers to the non-generic specification obtained from G by instanciating the type parameter T with the type nat and the specification parameter S with the specification ospec.

Identifiers coming from a generic specification (in particular the name of the generic specification itself) must always be fully instanciated (i.e., followed by an argument list of apropiate lenght). For example, if pspec[ ... ] is a parametric specification, then one has to write G[nat, pspec[... arguments ... ]]. In this case the expression G[nat, pspec] is syntacically incorrect.

It is possible to apply a signature morphism in parallel with an instanciation. For instance G[nat, ospec] RENAMING f as g refers to G instanciated as before but with the obvious renaming applied to it. For theory expressions the renaming clause can also rename sort names. If the renaming clause is not present then the identity signature morphism is used.

If the renaming occurs inside an instanciation like in G[nat, pspec [ ... ] RENAMING f as g] then the domain of the signature morphism pspec [ ... ] RENAMING f as g can be derived from the context. In this example it is ospec because of the declaratin of G. Theory expression are also used in refinements. There it may be necessary to specify the domain of the signature morphism with the from VIEW ... or GENERATE ....

Let pspec [ ... ] RENAMING f AS g denote a signature morphism with domain ospec. Then one can equivalently write VIEW pspec [ ... ] AS ospec RENAMING f AS g or GENERATE ospec FROM pspec [ ... ] RENAMING f AS g.


Specification abbreviations

Similar to type abbreviations from the metasymbol typedef one can define new names for long theory expressions. This makes partial instanciations possible.


    SPEC identifier [ parameterlist ] EQUAL theoryexpression 
And specdef is a top level declaration:
  | specdef
Let G[T : Type, S : ospec] be a generic specification, where ospec is some specification without parameters. One obtains the partial instanciation Gnat as

SPEC Gnat[S : ospec] = G[nat, S]

If one of the theory expressions has new type parameters that should remain free one has to declare them like in

SPEC Gp[T : Type, P : ... ] = G[T, pspec[P]]

Partial operations

It is possible to declare operations, in particular constructors and methods, as partial. In this case they get a semantics as partial functions.


I don't know yet. I have two ideas:


The intention is clear. But how to represent that best in PVS?


Besides specifications it is possible to state refinements. A refinement consists of an abstract specification, a concrete specification and a signature translation. As semantics a refinement generates proof obligations.


    REFINEMENT identifier COLON theoryexpression [ BEHAVIOURALLY ] REFINES identifier [ parameterlist ] 
where refinement is a top level declaration
  | refinement
Note, that in refinements the declaration order is somehow reversed. The theory expression may contain type and theory parameters which are declared in the prameterlist.

Open Problems

First-order restriction

In CCSL 3 one can restrict the logic to first order logic. What precisely belongs to the first order fragment is not yet defined.


In CCSL 3 various restrictions and extensions can be specified inside the CCSL file (instead of as compiler switches) in the form of directives. There are at least the following directives:

Home Science Overview All Publications Talks PhD CCSL Robin

last modified on 20 Sep 2011 by Hendrik