comments on v0.96 of CASL

[Don Sannella <dts@dcs.ed.ac.uk>]

Most of what I have to say about 0.96 has already been said by others,
so I will just mention two things: local definitions in formulae and
linear visibility.

1. Local definitions in formulae

Maura wrote:
> I think that in Paris we decided to have in (that is: to propositively add
> it to) the new summary a construct to have shortcuts for long terms to be
> used in axioms, something like
>   let t=f(hgfhf(jjj,yuyt,sdfdsf,........) in
>   t=g(t,t)=>p(t,f(t))
> whose semantics is expected to be "to add to the local environment a
> partial constant t of the expected sort and the axiom t=.... and use it to
> evaluate the axiom, discharging then the constant".
> 
> I didn't find any trace of this in the summary.
> Is this because
> a) my memory is not anymore as it used to be ;-)
> b) some different decision was made afterward,
> c) we leave it to the concrete syntax (...?...I dislike to have a concrete
> construct that cannot be mapped into any abstract one, as we don't have
> local declarations in basic items)
> d) I simply missed it?

Let me merely say that I agree strongly with Maura (and Michel): we
need some way of abbreviating terms in formulae.  And in reply to (c)
above, it is certainly no good to leave such things to concrete
syntax.

2. Linear visibility

Peter wrote:
> > then any real need
> > for non-linear visibility would disappear. As far as I can see, in all
> > other cases we can (and in my view, we should) write basic specs so
> > that linear visibility is maintained.
> 
> What is the motivation for linear visibility: methodology, semantics,
> tools, other languages, ...?

I think a much better question is: what is the motivation for
NON-LINEAR visibility?  Here is the answer:

  So that it is possible to write the syntax of a language like CASL
  without having to present it bottom-up.

That's the whole answer, as far as I have been able to determine!

[See also the draft of a Rationale for CASL visibility and scope in my
own message, just sent.  --PDM]

Most languages I have seen (both specification and programming
languages) use linear visibility.  Of course there are exceptions, but
I think it is fair to say that they are just that: exceptions.  The
semantics of linear visibility is a bit simpler.  Tools are a bit
simpler with linear visibility.  Linear visibility makes things easier
to read because one doesn't need to scan the entire text to find a
declaration of some mystery symbol.

I have heard people say that non-linear visibility is useful for a
specifier who finds in the course of writing an axiom that some
auxiliary function is convenient and can't be bothered to move the
declaration to a point before its first use.  I must say that I find
this unconvincing in the extreme.  Specification is not like hacking,
and people who write specifications will be willing to keep things in
a proper order -- this is surely the least of their problems!

That said, I can accept non-linear visibility, but I would find it
easier to swallow if people wouldn't pretend that it is somehow
forced.

Best regards, Don