[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Some subtleties about structured specs
Dear semanticists,
I hope that all of you will also get some nicer Xmas presents
than the following ones:
There are some minor subtle issues about the semantics of CASL that need
some discussion. Unfortunately, in most cases this also has possible
impact on the language design. Therefore, I would like to have your attention
for a moment. The issues are:
1) Default mechanism for symbol maps
2) Interaction of renamings, revealings and hidings with the local environment
3) Semantics of unions
4) Simplification of the semantics of structured specifications
The first three issues also have impact on the language design.
The issues have to be clarified before a final version of the semantics
of structured specifications can be produced.
Sorry for bothering you with this stuff now, but the semantics
of symbol maps is really a bit intricate (I revised it several times).
The third issue was found only when feeding the basic datatypes
through the static analysis.
Greetings,
Till
1) Default mechanism for symbol maps
------------------------------------
The Summary says on page 35:
A mapping of symbols in $|\Sigma|$ determines the morphism from
$\Sigma$ that extends this mapping with identity maps for all the
remaining symbols in $|\Sigma|$. In the case that the signature
morphism does not exist, the enclosing construct is ill-formed.
The semantics as it is in S-9 closely follows the summary.
However, this is probably not what was originally intended:
Consider the specification
spec Sigma =
sort s
ops f:s->s
with s |->t
end
Of course, we expect that f:s->s is mapped to f:t->t,
thus, "the remaining symbols in $|\Sigma|$" are *not*
mapped identically. Rather, the remaining symobls
in $|\Sigma|$ are mapped to symbols with the same name
(where the name of a symbol is its unqualified part),
while the qualification may change accordingly.
This has been formalized in S-10, and it should, in my opinion,
also be incorporated in the summary and the semantics.
2) Interaction of renamings, revealings and hidings with the local environment
------------------------------------------------------------------------------
During the work on the library of basic datatypes, I encountered
the following situation:
spec
Field [DefineField with sort Elem, ops 0, 1, __+__, __ * __ ] =
Ring [DefineRing] with sort RUnit, ops inv, __ - __
then
Group [ConstructField fit sort Elem |-> NonZeroElement,
ops 0 |-> 1,
__+__ |-> __*__
]
with
sort NonZeroElement,
ops __ - __ |-> __ / __,
inv |-> multInv
Here, the renaming of __ - __ is ambiguous: it can affect
both the __-__:Elem*Elem->Elem which is there in the local
environment (coming from Ring), and the
__-__:NonZeroElement*NonZeroElement->NonZeroElement
coming from the instantiation of Group.
Now currently, the semantics resolves this ambiguity by
just trying to rename all profiles uniformly.
But then, it is found that the profile __-__:Elem*Elem->Elem
is contained in the local environment; and since it
is forbidden to rename things from the local environment,
the renaming is actually not well-formed according
to the static semantic rules.
For the above specification, there is an ad-hoc solution:
enclose the instantiation of Group into a closed spec:
spec
Field [DefineField with sort Elem, ops 0, 1, __+__, __ * __ ] =
Ring [DefineRing] with sort RUnit, ops inv, __ - __
then
closed
{
Group [ConstructField fit sort Elem |-> NonZeroElement,
ops 0 |-> 1,
__+__ |-> __*__
] %% modified, since fitting views are not supported yet
with
sort NonZeroElement,
ops __ - __ |-> __ / __,
inv |-> multInv
}
Another, perhaps more staisfactory, solution would be to change
the semantics such that the profile __-__:Elem*Elem->Elem
is automatically excluded from the disambiguation procedure
because it is in the local environment.
This would complicate the institution-independent semantics (see S-10)
a bit at those points where a signature morphism is constructed
out of a raw symbol map: These constructions would now get an
extra parameter, namely the (set of symbols of) the local environment.
The summary is quite neutral wrt this question. It just says in 6.1.1.,
p.37f.:
The morphism must not affect the symbols already declared in the
local environment, which is passed unchanged to \Meta{SP}.
So we should consciously decide what to do here.
3) Semantics of unions
----------------------
With the semantics in S-9, a union of a specification
containing f:s->s with a specification containing f:s->?s
is ill-formed.
In S-10, an alternative definition of CASL as an institution
with symbols is proposed in section 6.1, page 23.
The idea is that totality or partiality of an operation
is not visible at the level of symbols, i.e. both
f:s->s and f:s->?s lead to the same symbol.
This would have the effect that a union of a specification
containing f:s->s with a specification containing f:s->?s
would be well-formed, and in the union, we would get f:s->s.
This effect corresponds to what Eric Wagner has proposed in
his WADT99 talk.
As far as I can see, the summary is neutral wrt. this question,
so again, there is a conscious decision to be made what to do.
After that, this should be clarified in the summary (in one
of the both ways), and the semantics should follow that.
4) Simplification of the semantics of structured specifications
---------------------------------------------------------------
(This has no effect on language design.)
Sasha has proposed to simplify the semantics of structured specifications
in the following way:
Currently, the rules for the static semantics produce a signature
inclusion, which is viewed as a signature extension (namely, the
local environment signature is extended with some new stuff
coming from the construct under consideration).
Now it would be much simpler just to return the *target* of the
signature inclusion. Since the source of the signature inclusion
(the local environment) is already fed into the rules, it is
always possible to reconstruct the signature inclusion:
both source and target are at hand.
Hubert and I have checked the structured and architectural
semantics wrt to this modification. In all places, the changes
are straightforward, and the results rules are simpler than
the present ones.
-----------------------------------------------------------------------------
Till Mossakowski Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen till@informatik.uni-bremen.de
P.O.Box 330440, D-28334 Bremen http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------