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

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

Dear Peter, thanks for thinking of me, but im afraid im not the one to get
into the semantics of CASL!  But i would like to note that OBJ3 has simple
rules for principle sort etc. for structured specs, and they seem to work just
fine in practice.  OBJ3 does indeed have (what you call) generic views, so
LIST[LIST[NAT]] and the like do indeed work.  Im surprised that the CoFI
community hasnt spent a little time studying such things; by the way, CafeOBJ
also has these features.

While im in this by-the-waying mood, Id like to mention that Ive been very
impressed by some of recent examples done in CafeOBJ, using hidden algebra to
verify behavioral properties of some rather complex distributed object
systems.

== joseph

******************************************************************************
>Resent-From: Peter Mosses <mosses@csl.sri.com>
>Resent-Date: 28 Aug 1998 13:03:29 -0700
>Date: Fri, 28 Aug 1998 02:17:19 +0200 (MET DST)
>From: "Peter D. Mosses" <pdm@daimi.aau.dk>
>Reply-to: pdmosses@brics.dk
>
>Dear Joseph,
>
>First of all, thank you for taking the time to read and respond to the
>recent messages concerning views in CASL.
>
>You wrote:
>
>>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.
>
>It was with considerable reluctance that I proposed the removal of
>implicit fitting views from CASL.  Personally, I fully agree with your
>arguments about the advantages of (e.g.) LIST[NAT] over LIST[NATasELEM]
>regarding perspicuity (I assume that this was the "baby" above?).
>I really would have liked to see something close to the OBJ3 treatment
>of views in CASL v1.0.
>
>However, as far as I recall, *generic* fitting views (our
>"crocodile"?)  were not actually implemented in OBJ3 - please correct
>me if I'm wrong on that (or on anything else, of course!).  But if one
>is allowing non-generic views to be left implicit, it seems natural to
>do this for generic views too (thus allowing LIST[LIST[NAT]] -
>provided that the generic views to be used are uniquely determined).
>And it is here that we appear to run into difficulties with the
>semantics.
>
>We did consider adopting OBJ3-style default views, but the notion of
>the principal sort of a module seemed difficult to extend in a uniform
>way to structured specifications.  Now that implicit views are to be
>eliminated from CASL, we should perhaps reconsider default views,
>simply to allow users to write LIST[NAT], etc.  But we are getting so
>close to finalizing CASL version 1.0 that there isn't much time left
>for us to make a deeper investigation of this issue...  
>
>However, if someone (such as yourself!) could make a definite proposal
>for how to incorporate OBJ3-style views in CASL - with examples to
>demonstrate advantages over the current proposal, and with a
>straightforward semantics - there should still be a chance of
>adjusting the design before version 1.0 becomes frozen, I hope.
>
>Hoping for a positive - and quick - response,
>
>Best regards,
>
>Peter