Re: Semantical domain for SPEC

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

Dear All,

Till things along the same lines as me, except that faster (or at
least, he's much better organized and writes things down faster!)
Thanks Till!

Only one additional comment: I think it should be made clear, either
in the structure of the semantic domain for SPEC, or as an extra
condition somewhere, that we want here actually two semantic
functions: one working on signatures, to determine the result
signature (if any) independently of the class of models of the
argument, and dependently only on its signature part, and another
where the resulting class of models (if any) is determined. The first
would perform, intuitively, some decidable static analysis, the other
would corrsspond to the "real semantic semantics" :-) (model-theoretic
semantics).

I can see only one point where this may raise some doubts: when
instantiating generic specs (or parameterised units) to arguments via
fitting morphisms, we would be forced to accept "statically"
everyhting where just the signatures fit, and then
"model-theoretically" still throw out instantiations where the
required model-class inclusion would be checked.

Alternatively here, we may require that the first static functions
really determines well-formedness, and that the model-theoretic
function is defined whenever the static function is defined. Then
violating some semantic "fitting" conditions (in instantiation of
generic specs --- the story is a bit different in applying paramteric
units to arguments) would result in inconsistency rather than in
ill-formedness.

As for BASIC-SPEC: this kind of "incremental view" of specifications
is natural to handle basic items one by one as well. So, if I may
intrude a territory not assigned to me, i would suggest that a similar
semantic function is adopted for basic items as well (except that
something special must be done to propoerly take care of extra context
stuff like variable declarations).

Best regards,

Andrzej