CoFI semantics

[Alexandre Zamulin <zam@cs.usm.my>]

[Let me take this opportunity to announce that CoFI semantics note
S-5, entitled "Permissive Subsorted Partial Logic in CASL", has been
updated.  The new version is a paper to appear in Proc. AMAST'97.  To
find it, go to the CoFI home page (www.brics.dk/Projects/CoFI/) and
follow the link under "Latest News".   -- DTS]

Here are a few comments on the semantics of structured specifications
in note S-6.

1. Page 48 and in the sequel.

In the previous chapters the pre-order symbol $\leq_S$ is always suppled 
with a subscript, in this chapter it is never supplied with a sub-script. 
I believe that the difference in notation should be eliminated.

2. Page 48.

I understand that id_S is the identity function on S; I believe, however, 
that is should be indicated explicitly.

3. Page 48.

\sigma^S\union id_S

The function union operation here is different from that one used in the 
previous chapters. I believe that it should be defined with the use 
of a different symbol. It should be noted which result is produced if 
both S and \bar{S} contain the same sort symbol.

4. Page 52.

"be" is missing in 

Each signature extension $\Delta$ is required to self-contained..

5. Page 53.

$\Delta$ is required to be an enrichment relative to $\Sigma$. 

Is \Delata really an enrichment? In the previous chapters an enrichment 
was denoted by (\Delta,\Psi). Denoting it by \Delta in this chapter is 
very confusing. 

Regards,

Alexandre. 

----------------------------------------------------------------------
Alexandre Zamulin                              e-mail: zam@cs.usm.my
School of Computer Science                     fax, phone:+60 4 6573335
University Sains Malaysia
11800 Penang, Malaysia
-----------------------------------------------------------------------