3 Semantic Annotations

We propose two different semantic annotations on extensions, namely %def (for "definitionally") and %cons (for "conservatively"). A discussion of the rôle of conservative and definitional extensions and further references can be found in [Mai97]. Semantically, a conservative extension

SP1

then %cons

SP2

In case of a definitional extension

SP1

then %def

SP2

Both annotations are also possible at the beginning of the body of a named parameterized specifications, since the body is an extension of the parameters:³

SP [SP1] ... [SPn] =

%cons

BODY

and

SP [SP1] ... [SPn] =

%def

BODY

The typical example for a definitional extension is the introduction of derived operations or predicates. Consider e.g. the partial order < in the specification BooleanAlgebra of [RM99]:

spec

DefineBooleanAlgebra =

sort

Elem

ops

0:Elem;
1:Elem;
__ |¯| __:	Elem ×Elem -> Elem,
	assoc, comm, unit 1;
__ |_| __:	Elem ×Elem -> Elem,
	assoc, comm, unit 0;

vars

x,y,z:Elem

%%

"adjointness":

.

x |¯| ( x |_| y) = x

.

x |_| ( x |¯| y) = x

%%

Zero and One:

.

x |¯| 0 = 0

.

x |_| 1 = 1

%%

distributive laws:

.

x |¯| ( y |_| z) = (x |¯| y) |_| ( x |¯| z)

.

x |_| ( y |¯| z) = (x |_| y) |¯| ( x |_| z)

%%

existence of an inverse element:

.

exists x': Elem . x |_| x' = 1 /\ x |¯| x' = 0

end

spec

BooleanAlgebra

[DefineBooleanAlgebra with sort Elem, ops 0, 1,__ |¯| __, __ |_| __] =

%def

SigOrder with preds __ < __,__ > __,__<__,__>__

vars

x,y:Elem

%%

induced partial order:

.

x < y <=> x |¯| y = x

end

The laws on the operations 0,1, |_| , |¯| in the specification
DefineBooleanAlgebra describe a class of models (boolean algebras), which are all partially ordered in a canonical way. Thus, in BooleanAlgebra the partial order can be defined in terms of the operations of boolean algebras, and there is a unique choice for the extension of a boolean algebra to a partially ordered boolean algebra.

Another aspect of the annotation %def arises in combination with a view. It is an established principle in mathematics to define an abstract concept like a Boolean algebra in terms of the weakest possible axioms. This makes it easy to prove that a concrete structure like the powerset of a set is an instance of an abstract concept. In CASL the property "to be an instance of" is expressed by a view. Thus on the one hand we would like to have a view from the specification BooleanAlgebra to the specification FinitePowerSet (see [RM99] for this specification) where the proof obligations only have to deal with the axioms that define a Boolean algebra, i.e. the derived predicate < is out of scope. On the other hand, having established this view we would like to speak about a partial order in the specification FinitePowerSet, which arises "automatically" from this view.

We suggest to reflect this idea in CASL as follows. As a view from SP₁ to SP₂ has to map all symbols of SP₁ on symbols of SP₂, we split the specification of a Boolean algebra in two parts: the specification DefineBooleanAlgebra introduces only the operations 0,1, |_| , |¯| and their axioms, while the specification BooleanAlgebra extends the former definitionally by the predicate < (see above). Then we relate the specifications DefineBooleanAlgebra and FinitePowerSet by a view:

view

DefineBooleanAlgebra_in_FinitePowerSet:

DefineBooleanAlgebra

to FinitePowerSet ... =

sort

Elem ^_|-> FinitePowerSet[X],

ops

0 |-> {},

1 |-> X,

__ |¯| __ |-> __ n __,

__ |_| __ |-> __ u __

end

spec

FinitePowerSet_with_BooleanAlgebra ...=

BooleanAlgebra

[ view DefineBooleanAlgebra_in_FinitePowerSet ]

end

A main use of the annotation %cons is to specify those intended consequences⁴ which should follow, in the specifier's view, from the specification. This can help in detecting errors in the specification, namely in those cases where the intended consequences actually do not follow from the specification. For example, look at the specification FiniteSet from [RM99]:

spec

FiniteSet[Elem]=

...

vars

x: Elem; S,T,U: FinSet[Elem];

...

%%

S c T:

.

{} c S

.

set(x) c S <=> x  elem_of S

.

(S u T) c U <=> S c U /\ T c U

...

then

%cons

vars

x: Elem; S,T: FinSet[Elem];

.

S c T <=> ( forall x: Elem . x  elem_of S => x  elem_of T )

end

Another example for the annotation %cons is the above discussed specification FinitePowerSet_with_BooleanAlgebra. As we mentioned in this specification the partial order < is not related with set inclusion c , although these predicates are equivalent. Thus we could add this property using a conservative extension:

spec

FinitePowerSet_with_BooleanAlgebra ...=

BooleanAlgebra

[ view DefineBooleanAlgebra_in_FinitePowerSet ]

then

%cons

vars

S,T: FinitePowerSet[X]

.

S < T <=> S c T

end

In some cases, it is more convenient to use a view to specify intended consequences. For example, to state that the specification BOOLEAN of [RM99]

spec

Boolean =

free type

Boolean ::= TRUE | FALSE

%%

intended system of representatives:

%%

TRUE, FALSE

ops

NOT__ :	Boolean -> Boolean;
__AND__, __OR__ :	Boolean ×Boolean -> Boolean,

%prec

__OR__ < __AND__

vars

x,y,z:Boolean

.

NOT(FALSE)=TRUE

.

NOT(TRUE)=FALSE

.

FALSE AND FALSE = FALSE

.

FALSE AND TRUE = FALSE

.

TRUE  AND FALSE = FALSE

.

TRUE  AND TRUE = TRUE

.

x OR y=NOT(NOT(x) AND NOT(y))

end

spec

Boolean =

...

then

%cons

DefineBooleanAlgebra

with

0 ^_|-> FALSE,

1 ^_|-> TRUE,

__ |_| __ ^_|-> __OR__,

__ |¯| __ ^_|-> __AND__

end

view

BOOLEAN_is_a_BooleanAlgebra :

DefineBooleanAlgebra to BOOLEAN =

ops

0 ^_|-> FALSE,

1 ^_|-> TRUE,

__ |_| __ ^_|-> __OR__,

__ |¯| __ ^_|-> __AND__

end