Object-oriented specification

Within the SoS group an experimental object-oriented specification language CCSL, for Coalgebraic Class Specification Language has been developed together with the Technical University of Dresden. A class specification in CCSL contains the following four main parts:

• declaration of methods, as coalgebraic functions acting on a state space Self;
• assertions, constraining the behaviour of these methods;
• initial states;
• assertions, constraining the behaviour of the initial states.

Begin queue[A : TYPE] : CLASSSPEC
   METHOD
     size : self -> nat;
     push : [self, A] -> self;
     pop : self -> Lift[[A, self]]

   ASSERTION SelfVar x:Self
     size_push :
       FORALL(a:A). x.push(a).size = succ(x.size);

     size_pop :
       CASES x.pop OF 
         bot : x.size = 0;
         up(y) : proj_2(y).size = pred(x.size)
       ENDCASES;

     pop_push :
       FORALL(a:A) .
         CASES x.push(a).pop OF
           bot : FALSE;
           up(y) : 
             CASES x.pop OF
               bot : proj_1(y) = a
                       AND
                     proj_2(y) ~ x;
               up(z) : 
                 proj_1(y) = proj_1(z)
                   AND
                 proj_2(y) ~ proj_2(z).push(a)
             ENDCASES
         ENDCASES;

   CONSTRUCTOR
     new : Self

   CREATION
     pop_new : new.pop = bot;
END queue

• Construction of models of a specification. This often reveals errors in the original specification. In the QUEUE example one can define a model with list[A] as state space Self.
• Theory development, i.e. derivation of consequences of the assertions in a specification. Typically, proving class invariants, like in the QUEUE example where one can show that `the size is non-negative' is an invariant (i.e. a property, which, once it holds, is maintained by all methods).
• Establishing refinements between specifications. Refinements may be seen as `relative models', where a model of one ("abstract") specification is constructed from a model of another ("concrete") specification. Invariants often play a crucial role in such refinements.

Some further features of CCSL are:

• The combined interfaces of the methods in a class specification give rise to an "interface" functor. A coalgebra of this functor gives an interpretation of the methods of the class.
• Associated with the interface functor of a class there are tailor-made definitions of invariance and bisimulation for the class. These definitions are automatically generated by the CCSL compiler.
• Based on the definition of invariance, appropriate definitions of Box (henceforth) and Diamond (eventually) are generated for each class. This enables the use of temporal logic for each class, for example for expressing safety and liveness properties.
• As structuring mechanisms between class specifications in CCSL one can use inheritance and aggregation (enabling the use of classes as `types' in other classes).
• Class specifications may be parametrised by types and by values, but not by specifications.
• Data type definitions (with initial semantics) can also be used in CCSL, enlarging the collection of possible interface types.

The CCSL language and compiler are currently maintained in Dresden. More information can be found there.