Science Overview
All Publications
Talks
PhD
CCSL
Robin
CCSL home page
Legacy Version 3 Discussion
The extensions discussed on this page comprise
genericspec:
BEGIN identifier [ parameterlist ] COLON [ modifier ] SPEC
{ section }
END identifier
modifier:
LOOSE
| FINAL
| INITIAL
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
| CCSL 2.x | CCSL 3 |
|---|---|
| FINAL CLASSSPEC | FINAL SPEC |
| CLASSSPEC | LOOSE SPEC |
| ADT | INITIAL SPEC |
sortsection:
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.
operationsection:
OPERATION operation { SEMICOLON operation }
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.
extendsection:
EXTENDING identifier [ argumentlist ]
{ COMMA identifier [ argumentlist ] }
Extensions are considered as syntactical sugar: The contents of
the named specification is instanciated and copied.
renamingsection:
RENAMING renaming { andorcomma renaming }
renaming:
identifier DOUBLECOLON idorinfix AS idorinfix
andorcomma:
AND
| COMMA
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.
parameterlist:
OBRACKET parameters { COMMA parameters } CBRACKET
parameters:
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).
argumentlist:
OBRACKET argument { COMMA argument } CBRACKET
argument:
type
| theoryexpression
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.
specdef:
SPEC identifier [ parameterlist ] EQUAL theoryexpression
And specdef is a top level declaration:
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]]
refinement:
REFINEMENT identifier COLON theoryexpression [ BEHAVIOURALLY ] REFINES identifier [ parameterlist ]
where refinement is a top level declaration
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.
Home
Science Overview
All Publications
Talks
PhD
CCSL
Robin