comments on 0.93: variable declarations

[reggio@disi.unige.it]

VARIABLE DECLARATION

Following the standard in algebraic specification, it would be
convenient to allow the user not to list the outmost universally
quantified variables in axioms, providing a construct for global
declaration of variables.

Thus, we suggest to add to X a mechanism for global variable
declarations (global w.r.t. the axioms of a BASIC_SPEC).

[It appears that this issue has not yet been discussed in the Language
Design Task Group.  This may be because those who would like to see
them didn't notice that the VAR-DECL construct in the abstract syntax
was not allowed as a BASIC-ITEM.  Would anyone who has arguments
against adding such a construct kindly advance them as soon as
possible.  Unless such arguments are forthcoming, I intend to include
variable declarations in v0.94 of the proposal, although the decision
about whether or not to include them may have to be left to the
Edinburgh meeting.  --PDM]

A BASIC_SPEC using such a mechanism may be as follows:

...
var  x1, x2: srt
var  y1, y2: srt'

ax  for1
ax  for2
ax  for3

where such BASIC_SPEC stands for the following one
written using formulae with explicit universal quantifiers

...
ax  forall x1, x2: srt
    forall y1, y2: srt'
        for1
ax  forall x1, x2: srt
    forall y1, y2: srt'
    for2
ax  forall x1, x2: srt
    forall y1, y2: srt'
    for3

Global variable declarations are, for example, present in OBJ.

The relevance of the use of such mechanism to allow to write coincise
and clear specifications should be clear.  However you can consider
e.g. the case of conditional/equational specifications, where you are
oblige to use first-order quantifiers, instead of writing plain
(conditional) equations

To give a real example, in a specification of a case study,
that I have done, the following variables

var  id id1 id2 id3 id4 id5: device_ident
var  fid fid': fun_unit_ident
var  dsch dsch1 dsch2: devices_schema
var  fs fs': functional_unit_schema
var  ma: management
var  a a' x x': automatism
var  l: lab_automatism
var  opr: operation
var  ba bb: bar
var  ds: devices
var  sch: station_schema
var  ba bb: bar

are more or less all used in almost 30 axioms.  Without a global
variable declaration mechanism I have to write them almost 30 times,
or I can write them only once but I have to join toghether all 30
axioms by the ``and'' combinator.

Furthermore the global variable declaration mechanism helps to name
the variables in a coherent way inside each BASIC_SPEC and to avoid to
use in different axioms in a BASIC_SPEC or also in the same axiom
different names for the same quantity.

I also suggest to drop the sentence ``The variable declared by a
quantifier ... allowing variables to be overloaded.'', since, from a
methodological point of view, for me it is better to avoid to do what
it is suggesting.

===================================================================

Gianna Reggio
Dipartimento di Informatica e Scienze dell'Informazione
Universita' di Genova
Via Dodecaneso 35 - 16146 Genova (Italy)
Phone: +39-10 3536702
Fax: +39-10 3536699
email: reggio @ disi.unige.it