Re: [CoFI] Revised proposal for CASL Views, Imports

[Joseph Goguen <goguen@cs.ucsd.edu>]

Dear Hubert,

You are right, but my understanding of the rather extensive email discussions
that went along with the proposal was that a wide range of alternatives were
being considered, and my commentary is rather directed to aspects of those
discussions than to the final proposal.  In my opinion, the final result of
this process has been to throw out the baby along with the crocodile and the
bathwater.

-- Joseph

******************************************************************************
> Date: Thu, 6 Aug 1998 21:21:39 +0200 (MET DST)
> From: Hubert Baumeister <hubert@mpi-sb.mpg.de>
> 
> Joseph Goguen wrote:
> > 
> > In regard to "implicit fitting views", I would like to make three simple
> > observations:
> > 
> 
> It should be noted that implicit fitting views, as was proposed 
> for CASL and now abandoned, are different from default views of 
> OBJ. While implicit fitting views depend on views explicitly 
> defined by the user, default views in OBJ, please correct me if I 
> am wrong, only depend on the source and target specifications of 
> the view.
> 
> Here is an example:
> 
> spec POSET = sort T
>              pred __<=__ : T * T
>              axioms ...
> 
> spec NAT = sort N 
>            pred __<=__, __>=__ : T * T
>            ...
> 
> spec G[POSET] = ...
> 
> view NATAsPOSET1 : POSET -> NAT = T |-> N, <= |-> >=
> 
> spec SP1 = G[NAT]
> 
> With implicit fitting views, G[NAT] depends on the presence of a 
> unique, user defined view from POSET to NAT, which, in this 
> case, is NATAsPOSET.
> Then G[NAT] is equivalent to G[view NATAsPOSET], which is 
> equivalent to G[Nat fit T |-> N, <= |-> >=].
> 
> With default views, G[NAT] does not depend on the existence of 
> NATAsPOSET1; the default view from POSET to NAT only depends on 
> the principle sorts of POSET and NAT, which are T and N (by the 
> definition of principle sort in OBJ). Then G[NAT] is equivalent 
> to G[NAT fit T |-> N, <= |-> <=] (of course we can omit mappings 
> of the form s |-> s in CASL and simply write G[NAT fit T |-> N]).
> 
> Now we might observe that there is a second view from POSET to 
> NAT, mapping <= to <= instead of >= to <=. Thus we add to the 
> above definitions the following definitions:
> 
> view NATAsPOSET2 : POSET -> NAT = T |-> N, <= |-> <=
> 
> spec SP2 = G[NAT]
> 
> While the definition of SP1 was okay, because at the point of the 
> definition of SP1 there was only one explicit view definition 
> from POSET to NAT in the environment, ie. NATAsPOSET1, the 
> definition of SP2 is ill-formed, because at the point of the 
> definition of SP2 there exists two explicit view definitions from 
> POSET to NAT in the environment, ie. NATAsPOSET1 and NATAsPOSET2.
> 
> In general, the reader of a specification has to keep in mind all 
> the explicit view definitions to decide, without the help of 
> tools, whether G[NAT] is well-formed and what the view morphism 
> is (eg., T |-> N and <= |-> <= or T |-> N and <= to >=). With 
> generic views the situation is still more complex, as one has to 
> keep in mind all view-expressions that can be built from 
> generic views and non-generic views. 
> 
> Then, from the perspective of a reader of a specification, it is 
> easier to understand G[view NATAsPOSET1] than G[NAT], because the 
> reader can directly lookup the definition of NATAsPOSET1, for 
> instance using the search function of a text editor, instead of 
> looking at all view definitions to find the right one.
> 
> Regards,
>    Hubert
> 
> > 1. In my opinion, the issue of semantic correctness cannot be used as an
> > argument against implicit views, because exactly the same argument
> > applies to
> > all views: they are syntactic ("static") entities that should be checked
> > for
> > semantic correctness before they are used.
> > 
> > 2. The fact that achieving a fully general solution is difficult is not
> > a
> > valid argument against this feature, because it is possible to implement
> > something very simple that is still extremely useful, as demonstrated by
> > the
> > OBJ3 implementation, first described in my paper "Parameterized
> > programming"
> > and later in more detail in the OBJ3 manual.
> > 
> > 3. Countless users have found (what OBJ3 calls) default views to be
> > extremely
> > useful; in many cases the improvement in writability and readability is
> > very
> > dramatic.  It is not a valid argument to say that a default view can
> > always be
> > replaced by the name of an explicit view that is defined elsewhere,
> > because
> > there is still the effort of writing that view, or in the case of a
> > specification reader, of not only understanding the view, but also of
> > finding
> > it in the code.  Finding the significant parts of a large view that
> > mainly
> > consists of obvious mappings can be tedious.
> > 
> > -- Joseph
> > 
> [in my opinion, implicit fitting views (perhaps also implicit views)
> could and should be added to CASL once appropriate tools (that expand 
> them) have been developed and proven to be stable. A thesis in this 
> direction has just been finshed at Bremen (in the context of SPECTRAL) 
> but more work needs to be done. BKB]
> 
> -- 
>            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/