[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Suggestion for minor change of the concrete syntax
[message from Frederic Voisin at the end]
Michel Bidoit wrote:
> Dear CoFI Friends,
>
> Sorry to suggest this officially so late, but since we are still
> considering fixing minor details of CASL, I hope the following very minor
> suggestion can still be taken into account.
My understanding of the process is a bit different: we were asking for
any objections to the changes that have been incorporated in the CASL
v1.0.1-DRAFT Summary, rather than soliciting further fixes to details...
In fact Michel had previously mentioned his suggestion in e-mail to me
(as the editor of the Summary) and BKB (as the coordinator of the
Language Design task group), and I was already aware of BKB's support
for the suggestion. However, I did not think that it was advisable to
incorporate it in the v1.0.1-DRAFT Summary, for two reasons: it had
not previously been discussed in public; and it might have provoked a
flood of other minor suggestions concerning concrete syntax.
Anyway, with the appearance of the suggestion now on this mailing list
- just as I was preparing to remove the "DRAFT" status and install the
final v1.0.1 Summary - both my previous reasons for deferring
discussion of the suggestion have been undermined... I gather also
that the coordinator wishes to regard the suggestion as a valid
objection to the adoption of the present draft as the final v1.0.1
Summary.
N.B. Since there have been no other objections, all the changes
already implemented in the v1.0.1-DRAFT Summary have now been
adopted, and the question of whether or not to adopt further
changes related to Michel's suggestion is the ONLY topic left
open for discussion regarding v.1.0.1.
I suppose that we should allow a full 14-day discussion period for all
proposed changes to the design, even for such apparently minor
suggestions. That will take us to:
WEDNESDAY 5th JULY
(The full final CASL design was to be presented at the IFIP WG1.3
Meeting at Stanford, 29 June - 1 July, but I hope that the reviewers
will tolerate a delayed decision regarding this last detail of
concrete syntax.)
> Suggestion for change of the concrete syntax for local variable
> declarations (LOCAL-VAR-AXIOMS, see 2.2.2):
>
> Replace "var/vars" by "forall" (displayed \textbf{forall}).
>
> Note: This change is only at the level of the concrete syntax. No change at
> all of the abstract syntax is needed. Moreover, it has already been checked
> that from a tool point of view, the suggested change is harmless.
>
> Rationale: It seems that having the same keyword for global variable
> declarations and for local ones is a source of confusion, especially in the
> case of a global variable declaration followed by some axioms.
Let me remind those readers who are not fully familiar with the CASL
Summary that the input syntax for variable declarations and axioms in
a basic specification is (essentially) as follows:
vars v1,...,vn : s %{ declares the variables "globally"
for use in the subsequent axioms }%
vars v1,...,vn : s %{ declares the variables "locally"
. F1 for use in the axioms F1,...,Fn
... which are displayed with the "."
. Fn shown as a bullet }%
axioms F1;...;Fn %{ asserts F1,...,Fn for all values
of the globally-declared variables }%
forall v1,...,vn : s . F %% explicit universal quantification
(The following expresses my personal opinions as a participant of the
CoFI language design group, rather than as editor of the CASL
Summary. Sorry that it's a bit long-winded...)
I'm inclined to agree that the double use of "vars" can be confusing,
and that to replace the "vars" keyword in local variable declarations
with "forall" would be an improvement, the input syntax then being:
forall v1,...,vn : s
. F1
...
. Fn
Note however that when n=1, the input syntax above is then exactly the
same as for an explicit universal quantification! I would find it
quite difficult to explain why the "forall" gets displayed as a
keyword when this input occurs as a complete LOCAL-VAR-AXIOMS, but as
the mathematical symbol for universal quantification (LaTeX: \forall)
when it occurs as a single AXIOM in a list of AXIOMS.
MY PREFERENCE would therefore be to display "forall" uniformly as the
\forall symbol. (This may be non-optimal for sub-languages that omit
explicit quantification, but I think that we should give priority to
the smoothness of the full CASL concrete syntax design.)
I have one FURTHER RESERVATION concerning the concrete syntax of
variable declarations and axioms. Suppose that one wishes to
interleave operation declarations and axioms using local variable
declarations:
op f : ...
forall v1,...,vn : s
. F1
...
. Fn
op f' : ...
forall v1,...,vn : s
. F1'
...
. Fn'
If it happens that many of the local variable declarations coincide,
one may wish to factorize them out as global variable declarations,
and perhaps expect to be able to write:
vars v1,...,vn : s
op f : ...
. F1
...
. Fn
op f' : ...
. F1'
...
. Fn'
But the above is NOT CURRENTLY ALLOWED! When using global variable
declarations, each list of axioms must be introduced by the keyword
"axioms", and the axioms themselves separated/terminated by semicolons
";", thus:
vars v1,...,vn : s
op f : ...
axioms
F1;
...
Fn;
op f' : ...
axioms
F1';
...
Fn';
For a large specification, manually changing the style of axioms from
bullets to semicolons could be quite tedious. (I have experienced
this problem myself in practice: when using CASL as a meta-language
for specifying a Modular SOS of Action Notation - as illustrated in
the unpolished/unchecked document that I'm making temporarily
available at <http://www.cin.ufpe.br/~pdm/AS/2000/AN2v0.6-MSOS.ps.gz>
- although that is admittedly not a typical use of CASL...)
I would therefore like to PROPOSE an expansion of Michel's suggestion,
to allow not only:
axioms
F1;
...
Fn;
but also:
. F1
...
. Fn
as concrete syntax for AXIOMS.
I think that users would find it easy to accept that just as:
forall v1,...,vn : s
. F1
...
. Fn
can be regarded as a kind of extended universal quantification
governing several axioms, the syntax:
. F1
...
. Fn
corresponds to the case when the list of quantified variables is
empty.
Finally, if the above concrete syntax for AXIOMS were to be
introduced, one might question whether anyone would still use the
original concrete syntax:
axioms
F1;
...
Fn;
Note that the Bremen library of basic datatypes in CASL [CoFI Note
L-12] generally uses the LOCAL-VAR-AXIOMS construct, i.e. with
bullets, but switches to using AXIOMS with "axioms" and semicolons
when ground axioms are needed, e.g. in Basic/MachineNumbers. No big
problem, of course - merely a minor detail of the concrete syntax for
variable declarations and axioms that might be easily fixed...
I'm afraid that this will be my only input to the discussion of
Michel's suggestion, as I'm now very short of time for preparations
before I leave for a trip to the US on Friday. Let me therefore
stress here that if there are objections to my proposed amendment and
expansion of the suggestion, I can certainly live with the adoption of
Michel's original version.
-- Peter
[BKB: I agree with Peters extended proposal and would indeed prefer to
get rid of axiom alltogether]
____________________________________________________________
Peter D. Mosses * mailto:pdmosses@brics.dk
Centre of Informatics [local: pdm@cin.ufpe.br]
Federal University of Pernambuco http://www.brics.dk/~pdm
CP 7851 Tel:+55 81 271.8430x3057
Recife, PE, Brazil, CEP 50732-970 Fax:+55 81 271.8438
____________________________________________________________
* I'm visiting Recife until August 2000, while on leave from
BRICS & Dept of Computer Science, Univ of Aarhus, Denmark
======================================================================
From: Frederic.Voisin@lri.fr (Frederic Voisin)
To: cofi-language@brics.dk
Subject: Re: Suggestion for minor change of the concrete syntax
It is probably possible to accept both keywords for some time, marking
this use of "vars/vars/ as "deprecated" in the documentation.
frederic