   Go backward to 2 Introduction
Go up to Top
Go forward to 4 Parsing Annotations

# 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
means that each model of the specification SP1 can be extended to a model of the specification (SP1 then SP2). This implies that all SP1-sentences that follow from (SP1 then SP2) already follow from SP1, i.e. semantical consequence is conserved1.

In case of a definitional extension

 SP1 then %def SP2
we require that each model of SP1 can be uniquely extended2 to a model of (SP1 then 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:3

 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
%%
.
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 SP1 to SP2 has to map all symbols of SP1 on symbols of SP2, 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
The proof obligation associated with this view is only concerned with the operations 0,1, |_| , |¯| and their axioms. To obtain finally the intended relation between Boolean algebras and finite power sets we specify:
spec
FinitePowerSet_with_BooleanAlgebra ...=
BooleanAlgebra
[ view DefineBooleanAlgebra_in_FinitePowerSet ]
end
This specification is justified by the fact that the extension of DefineBooleanAlgebra by a partial order is definitionally. Note that in the specification FinitePowerSet_with_BooleanAlgebra the partial order < is not related with set inclusion c , although these predicates are equivalent. As we will see in the following, one can express this fact as a conservative extension.

A main use of the annotation %cons is to specify those intended consequences4 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
In this specification we have defined the predicate c in an operational manner. Thus, the formula S c T <=> ( forall x: Elem . x  elem_of S => x  elem_of T ) is not needed for the specification of c . However, it has the status of an axiom that should follow from the rest of the specification. If the proof of conservativeness of the extension succeeds, this is a double-check that the FiniteSet in fact specifies c properly.

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
indeed specifies a Boolean algebra, we could either write
spec
Boolean =
...
then
%cons
DefineBooleanAlgebra
with
0 |-> FALSE,
1 |-> TRUE,
__ |_| __ |-> __OR__,
__ |¯| __ |-> __AND__
end
or we could use a view:
view
BOOLEAN_is_a_BooleanAlgebra :
DefineBooleanAlgebra to BOOLEAN =
ops
0 |-> FALSE,
1 |-> TRUE,
__ |_| __ |-> __OR__,
__ |¯| __ |-> __AND__
end
Our intention is that a view relates different specifications while a conservative extension should be used to express properties of a specification which are not formalized elsewhere.
• 3.1 Syntactical Schemes for Conservative and Definitional Extensions

• CoFI Note: L-11 -- Version: 0.1 -- 11 March 1999.   