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

[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/