[CoFI] question

["Alexandre Zamulin" <zam@iis.nsk.su>]

[BKB: this message has been delayed, since I passed it on first to the
original addressee, Peter. Since he is busy, I am now trying to answer
it myself, hoping for you reaction if you do not agree]

Dear Professor Mosses,

I have a question concerning CASL. In Section 6.5, page 48, there is 
the following statement:

"If there are two compound sorts with multiple components, and the 
number of components are the same, and each pair of corresponding 
components either consist of two identical IDs or of two sorts in
the subsort relationship, then there is also a subsort embedding 
between the compound sorts."

Let us now assume that we have a generic specification corresponding 
to the Pascal-like array type and we produce two compound sorts 
ARRAY(FromOneToTen, Nat) and ARRAY(FromOneToTwenty, Nat). Evidenty, 
we can easily specify that the sort FromOneToTen is a subsort of 
FromOneToTwenty. However, we cannot state for Pascal-like arrays that 
ARRAY(FromOneToTen, Nat) is a subsort of ARRAY(FromOneToTwenty, Nat). 
How do you handle this problem?

With best regards,

Alexandre.

----------------------------------------------------------------------
Alexandre Zamulin                         
Institute of Informatics Systems
Siberian Division of the Russian Academy of Sciences     
Lavrentieva 6                                        fax:    +7 3832
323494
Novosibirsk 630090                                   phone:  +7 3832
396258
Russia                                               e-mail:
zam@iis.nsk.su
----------------------------------------------------------------------

[BKB: 

dear Alexandre,

thank you for your interest in CoFI! I hope you will follow the
initiative and comment in the future!

As to you question: I think a better modelling would be to have a
supertype "Interval" or "Bounds" or so, of which "FromOneToTen" and
"FromOneToTwenty" would be subsorts, e.g. specified using a subsort
definition constraining the bounds. 

        type Interval ::= interval(low:Nat;high:Nat)
        ...
        sort FromOneToTen = {i:Interval . low(i)=1 /\ high(i)=10 }

Note that you can introduce new subsorts for a given sort later in CASL,
similar to object-oriented techniques.

        sort FromOneToTwenty = {i:Interval . low(i)=1 /\ high(i)=20 }

Best regards
Bernd 
:BKB]


-- 
________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner    courier mail only:
FB3 Mathematik und Informatik      MZH 8071, FB3
Universitaet Bremen                Universitaet Bremen
Postfach 330 440                   Bibliothekstr. 1
D-28334 Bremen                     D-28359 Bremen

Telefon: (+49) 421-218-3660        telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE       privat:  (+49) 421-25-1024
http://www.informatik.uni-bremen.de/~bkb
http://www.uni-bremen.de/~sppraum