Re: Scope of variables

[Hubert Baumeister <hubert@mpi-sb.mpg.de>]

Till Mossakowski wrote:
> 
> Dear all,
> 
> a question by Bernd made me realize that the current proposal
> for [SPEC] answers Hubert's question on page 9
>         Should variable declarations be put into the local
>         environment, maybe in a separate mapping for variable names?
> with "no", while Bernd in his examples assumes that the answer
> is "yes" and variable declarations are visible through EXTENSIONs.
> 
> I prefer a "no" here for simplicity, and actually on page 7,
> the scope of variable declarations is explicitly defined
> to be the enclosing BASIC-SPEC.
> 
> Greetings,
> Till

I think there is a difference between the local environment (LEnv) used
to construct BASIC-SPECs and SpecMod used in the semantic domain of
SPEC. As I see it, elements of LEnv have to store information about
declared variables, sorts, function- and predicate symbols and maybe
some more things, like sets of axioms.
Then the semantic domain of BASIC-ITEMs is a partial mapping from LEnv
to LEnv. 
If no information about variable declarations were available, how would
one decide in the following BASIC-SPEC that the equation in line 3 has
to be rejected, while the equation in line 5 is okay?

sort int
function f : int -> int
f(x) = 3
var x : int
f(x) = 3

In contrast, SpecMod has as elements pairs (\Sigma,M), where \Sigma is a
signature from the underlying logic and M a class of \Sigma-algebras.
Especially, \Sigma does not contain variable declarations (cf. section
2.2 page 9).

For the semantics of a BASIC-SPEC as a partial function from SpecMod to
SpecMod, first the initial local environment is constructed from an
element of SpecMod and then an element of SpecMod is extracted from the
environment resulting after applying the composition of the semantics of
the BASIC-ITEMs to the initial environment.
In the transition from elements of LEnv to elements of SpecMod some
information is lost, like information about declared variables. 

With the current definition of SPEC, variable declarations in the
OF-SPECs of an extension are not visible in the SPEC part of extension.
This would change if the semantics of SPECs are partial functions from
LEnv to LEnv. How difficult it is to use this kind of semantics for
structured specificatons mainly depends on the structure of LEnv.
I agree with Till, that for simplicity we should use partial functions
from SpecMod to SpecMod.

Hubert


-- 
           Hubert Baumeister
           MPI Informatik, Im Stadtwald, D-66123 Saarbr"ucken, Germany
    Phone: (x49-681)9325-220  Fax: -299
   e-mail: hubert@mpi-sb.mpg.de  
      WWW: http://www.mpi-sb.mpg.de/~hubert/