Go backward to 5.3 Static Semantics
Go up to 5 Our Proposal More in Detail
5.4 Semantics
The semantics of a parameter type consists of the semantics of the
overall specification and the set of its generic names (with their
profiles, if
needed)
The semantics of generic specifications is the space of partial
functions from
([[ SPEC ]]×[[ sig-morph ]])n into [[ SPEC ]] for any
non-null n.
Given a statically correct declaration
gen-spec-defn GSP gen-spec Par_1...Par_n Sp_Body
where each Pari is
Xi1...Xiki par-type Spi fixed-names Spi1...Spimi
.
the semantics of GSP is a partial function
f:([[ SPEC ]]×[[ sig-morph ]])^k -> [[ SPEC ]]
where k=SUMi=1n ki.
The result of f is defined iff
- Static correctness
-
For each argument (SpA,sigmaA), we have that the morphism
sigmaA maps the signature of the corresponding formal parameter into
that of
SpA leaving unaffected the fixed symbols.
In the following we call SpA the actual parameter and
sigmaA the fitting morphism.
- Dynamic correctness
-
For each argument (SpA,sigmaA), the reduct along
sigmaA
of the model class of SpA is a subset of the model class of the
corresponding formal parameter.
Notice that this, in particular, requires that the semantics of the
fixed symbols of an actual parameter, if any, is a refinement of the
semantics of the fixed part in the corresponding formal parameter.
If such result is defined, then it is the evaluation of the body
SpBody, where each occurrence of a generic meta-symbol has been replaced
by the symbol determined by the fitting morphisms (where no ambiguities
arise due to the use of referenced names and the restriction on the
redeclaration of generic)
and then evaluated in the current environment updated by the associations
of the actual with the formal parameters.
Equivalently, let <Sigma,M> be the evaluation of the body
SpBody in the current environment updated by the associations
of the translation of the actual parameter along the fitting morphism
with the formal parameters.
Then, the result of f is <Sigma',M'>, where Sigma' is
Sigma where each occurrence of a generic meta-symbol has been
replaced by the symbol determined by the fitting morphisms and M'
consists of all those Sigma'-models whose translation along the
union of the fitting morphisms belongs to M.
The semantics of a statically correct declaration
gen-spec-defn GSP gen-spec Par_1...Par_n Sp_Body
updates the environment by associating the name GSP with
the semantics of gen-spec Par1...Parn SpBody.
The semantics of a statically correct instantiation
gen-spec-inst GSP fitting-arg Sp_1 [sigma_1]... fitting-arg Sp_n [sigma_n]
in an environment associating GSP with f yields
f(<[[Sp1]],sigma1>,...,
<[[Spn]],sigman>), where sigmai
is the signature morphism extending sigmai by the identity on
the symbols that are not listed in it.
CoFI
Note: L-3 --DRAFT, Version 0.2-- 21 May 1997.
Comments to cerioli@disi.unige.it