The extensions discussed on this page comprise

- general specifications
- additional sections for
- generic specifications
- signature morphisms, specification values, and instanciations
- specification abbreviations
- partial operations, i.e., partial methods and partial constructors
- refinements
- restriction to first order logic
- Directives

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.genericspec: BEGIN identifier [ parameterlist ] COLON [ modifier ] SPEC { section } END identifier modifier: LOOSE | FINAL | INITIAL

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

- SORT
- OPERATION (superseeding METHOD and CONSTRUCTOR)
- AXIOM (superseeding ASSERTION and CREATION)
- THEOREM
- EXTENDING (possibly superseeding INHERIT)
- RENAMING (superseeding the current renaming clause)
- DEFINING
- lifting requests

CCSL 2.x | CCSL 3 |
---|---|

FINAL CLASSSPEC | FINAL SPEC |

CLASSSPEC | LOOSE SPEC |

ADT | INITIAL SPEC |

- What is used as semantics for loose specifications? Probably simply a set of functions that fulfill the Axioms. However this is quite different from loose class specifications in CCSL 2.x. Currently you get bisimulation, invariants, and coalgebra morphisms.

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).sortsection: SORT identifier { COMMA identifier }

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.

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.operationsection: OPERATION operation { SEMICOLON operation } operation: identifier COLON type | identifier COLON type ARROW type

- Assume a specification with final semantics in which all methods and constructors are declared in one OPERATION section. Does the compiler sort itself out what are methods and what are constructors?
- In CCSL 2.x bisimulations, invariants, and coalgebra morphisms neglect all declared constructors. Does bisimulation in CCSL 3 take those operations into account that have method type?

- For the semantics of final class specifications in CCSL 2.x it is essential to distinguish between assertions and creation conditions.
- Further for the construction of the final model assertion must contain a distinguished free variable.

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

- The relation to inheritance of class specifications is unclear. Depending on that the keywords INHERIT FROM are synonymous to EXTENDING.
- Multiple inheritance certainly makes sense. How about multiply extending the same specification?

In a renamingrenamingsection: RENAMING renaming { andorcomma renaming } renaming: identifier DOUBLECOLON idorinfix AS idorinfix andorcomma: AND | COMMA

- If one wants to inherit twice from the same specification one probably needs a renaming directly following the first inheritance. For this purpose it makes sense to keep the renamings from CCSL 2.x in CCSL 3 extensions as syntactic sugar (that expand to a sequence of extension and renaming sections).

A parameter declared with the keywordparameterlist: OBRACKET parameters { COMMA parameters } CBRACKET parameters: identifier { COMMA identifier } COLON [ variance ] TYPE | identifier { COMMA identifier } COLON [ variance ] identifier [ argumentlist ]

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).

- Consider the parametric specification
`list[ X : TYPE ]`, describing the lists over`X`. Should we allow theory parameters of the form`Y : list`, that is, you parametrise over arbitrarily typed lists? I tend to allow only fully instanciated apecifications as theory parameters. - Variances are probably necessary for theory parameters. At the moment it is not clear how to compute them.

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.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 ]

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`.

- The semantics of a signature morphism is the obvious renaming transformation on the class of models.
- The instanciation of a theory parameter
`S : ospec`with a theory expression`pspec [ ... ]`is only valid if the class of models of`pspec [ ... ]`is contained in the semantics of`ospec`. This condition is generated as proof obligation like a TCC in PVS.

Andspecdef: SPEC identifier [ parameterlist ] EQUAL theoryexpression

Letdeclaration: .... | specdef

`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]]`

- Enrich the type theory of CCSL with a "partial exponent",
e.g.,
`[nat -` nat]`denotes the type of partial functions on the natural numbers. Here`-``is the ASCII version of the half arrow. Other possibilities:`-/->`or`-/`or`-\`. - Define modifiers
`PARTIAL`and`TOTAL`similarly to`PUBLIC`and`PRIVATE`. Then`PARTIAL OPERATION`(or`PARTIAL CONSTRUCTOR`) declares parial items and`TOTAL OPERATION`total items. The default should probably be`TOTAL`.

where refinement is a top level declarationrefinement: REFINEMENT identifier COLON theoryexpression [ BEHAVIOURALLY ] REFINES identifier [ parameterlist ]

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.declaration: .... | refinement

- Should we really distinguish between assertional (aka modell-theoretic) and behavioural refinements?
- What about the parameter translation? I mean, is it possible
that the abstract spec
`Queue[X : Type]`is refined by the concrete`Array[Lift[X]]`, where`X`is a free type variable (implicitly univerally quantified)? - What is a refinement with a theory parameter?

- expert mode, for turning all errors into warnings
- pedantic mode, for accepting only strictly covariant functors
- first order, for restricting the logic to first order logic

Home
Science Overview
All Publications
Talks
PhD
**CCSL**
Robin

last modified on 20 Sep 2011 by Hendrik