Re: Labels before ALTERNATIVEs; Named Views

[Peter Mosses <mosses@csl.sri.com>]

[see also example of named views at end]

Till wrote:

> Kolyang has just adpated the Bremen parser to deal with labels.
> Here, the following question arose:
> 
> Was it a conscious decision to allow labels only before each item
> in a bullet- or semicolon-separated list of items, but not
> before an ALTERNATIVE (i.e. an item in a "|"-separated list)?

Well, perhaps only semi-conscious. :-)

> Currently,
> 
> spec Tree =
>   sort Tree ::= leaf(elem)
>                 | tree(%[left] Tree; %[right] Tree)
> end
> 
> is allowed, while
> 
> spec Tree =
>   sort Tree ::=   %[LeafCase] leaf(elem)
>                 | %[TreeCase] tree(Tree; Tree)
> end
> 
> is not allowed.

I suppose that it would be OK to allow the latter too.  The main issue
is that it should be easy to see what construct has actually been
labelled - which is why we don't allow labels at arbitrary places in
formulae and terms.  One probably doesn't think of `...|...' as
a construct itself, so in

 spec Tree =
   sort Tree ::=   %[mylabel] leaf(elem) | tree(Tree; Tree)
 end

one may perhaps guess that only the first alternative is labelled?

As time is short, I'll simply moderate the current over-specication in
C.5.2.1.  This issue is independent of the rest of the CASL design,
and what we allow could easily be adjusted in a future version.

-- Peter

PS 

Nobody has provided me yet with examples of the definition and use of
NAMED VIEWS!  I'm almost finished with updating the Summary to v1.0,
apart from checking that the previous examples (with Till's suggested
modifications) still parse OK.  If I get the examples of named views by
sometime on Wednesday (EU time) I may still manage to include them...
_________________________________________________________
Dr. Peter D. Mosses             International Fellow  (*)

Computer Science Laboratory     mailto:mosses@csl.sri.com
SRI International               phone: +1 (650)  859-2200 ! CHANGED
333 Ravenswood Avenue           fax:   +1 (650)  859-2844
Menlo Park, CA 94025, USA       http://www.brics.dk/~pdm/

(*) on leave from DAIMI & BRICS, University of Aarhus, DK
    also affiliated to CS Department, Stanford University
_________________________________________________________

From: Till Mossakowski <till@Informatik.Uni-Bremen.DE>
Message-Id: <199810211244.OAA21399@james.informatik.uni-bremen.de>
To: cofi-language@brics.dk, mosses@csl.sri.com
Subject: Examples for named views
Cc: till@james.informatik.uni-bremen.de
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Content-MD5: jWDiMoz67pl57jejVzbZew==

Dear Peter,

>Nobody has provided me yet with examples of the definition and use of
>NAMED VIEWS!  I'm almost finished with updating the Summary to v1.0,
>apart from checking that the previous examples (with Till's suggested
>modifications) still parse OK.  If I get the examples of named views by
>sometime on Wednesday (EU time) I may still manage to include them...

O.K. Here are some examples.


I have tried to make them compatible with the other examples,
so that the whole bunch of examples is self-contained (this
eases the understanding). In order to achieve self-containedness,
the specification

spec Elem =
  sort Elem
end

should be introduced just before Set1, and we need ordinary lists:

spec List[Elem] =
  free type
     List[Elem] ::= nil | cons(first :? Elem;rest :? List[Elem])
end

Then, we can write:

view Nat_as_Elem : Elem to Nat =
        Elem |-> Nat
end

view List_as_Elem[Elem] : Elem to List[Elem] =
        Elem |-> List[Elem]
end

spec List_Of_List_Of_List_Of_Nat =
        List[view List_as_Elem[view List_as_Elem[view Nat_as_Elem]]]
end

I find this syntax quite wordy. What about

spec ListOfListOfListOfNat =
        List[List_as_Elem[List_as_Elem[Nat_as_Elem]]]
end

i.e. FIT-VIEW has the same concrete syntax as SPEC-INST,
where the ambiguity between FIT-VIEW and SPEC-INST is resolved in such 
a way that both are mapped to SPEC-INST by the parser, and the static
semantic analysis has to map some SPEC-INSTs to FIT-VIEWs, depending
on the global environment?
(This kind of processing appears to be necessary for UNIT-SPEC-NAMEs
and SYMBs in SYMB-MAPs anyway.)


An example invloving a real check of model class inclusion:

spec Ord_Nat =
  Nat then
  pred __<__ : Nat * Nat
  vars m,n:nat
  axioms
    zero < succ(n)
    not n < zero
    succ(m) < succ(n) <=> m < n
end

view Ord_Nat_as_PO : {PO with T |-> Elem} to Ord_Nat =
        Elem |-> Nat
end
%% This view can be seen as requirement that Ord_Nat indeed
%% specifies a partial order. Thus defining the view would make 
%% sense even if the subsequent instantiation were omitted.

spec Nat_List_With_Order =
        List_With_Order[Ord_Nat_as_PO]
end
        
I assume that in Ord_Nat_as_PO, we do not need to write 

        __<__ |-> __<__ 
        
because the specification morphism is determined with the help 
of the last paragraph of chapter 5. The last paragraph on page 45 
could be a bit more explicit here, in particular, it should
be stated that the view definition is well-formed only if
the symbol map determines a singleton set of signature morphisms
(such that the unique element is a specification morphism).

(Editorial comment: Replacing T with Elem in PO would enable
us to omit "with T |-> Elem", which seems to be wortth while,
since this renaming does not illustrate so much.)

An example invloving imports (and re-using Nat_as_Elem):

spec Bounded_List (given Nat) [op bound:Nat] [Elem] =
  List[Elem] and Ord_Nat then
  op length : List[Elem] -> Nat
  vars x:Elem; l:List[Elem]
  axioms
    length(nil)=zero
    length(cons(x,l))=succ(length(l))
  sort Bounded_List[Elem] = {l:List[Elem] . length(l)<bound}
  type
    Bounded_List[Elem] ::= cons(first :? Elem;rest :?
Bounded_List[Elem])?
      %% the bevaviour of these operations is determined by overloading
end

spec Nat_Bounded_List =
  Bounded_List[Nat_as_Elem]
end

Peter, perhaps you can send me the whole bunch of examples
for re-checking once it is ready?

Greetings,
Till


P.S.

Here is an example explaining how to use parameters twice
(I think it is not so convincing, but this is not the fault
of the example, but of the "same name - same thing" principle,
which leads to some clumsiness in this case):

spec ELEM1 =
  ELEM with Elem |-> Elem1
end

spec ELEM2 =
  ELEM with Elem |-> Elem2
end

spec Pair[Elem1] [Elem2] =
  free type Pair[Elem1,Elem2] ::= pair(left:Elem1,right:Elem2)
end

view Pair1[Elem] : Elem1 to Elem =
        Elem1 |-> Elem
end

view Pair2[Elem] : Elem2 to Elem =
        Elem2 |-> Elem
end

spec NatPair =
   Pair[Pair1[Nat_as_Elem]] [Pair2[Nat_as_Elem]]
end
  
(To be really shorter than writing something like

        Pair[Nat fit Elem1 |-> Nat] [Nat fit Elem2 |-> Nat]
        
one would have to replace Elem by Monoid. If wanted, I can provide
such an example.)