[CoFI] Re: Examples of concrete syntax for CASL basic specs

[Andrzej Tarlecki <tarlecki@mimuw.edu.pl>]

I have had a brief look through the syntax proposals, and here are few
immediate points:

==============================================================================
--- I would prefer "opn" and "opns" rather than "op" and "ops": one
more letter does not seem to cost much, and in my view more
unambigously identifies "operation" (and puts the keyword further away
from "oops" :-)

--- as already noted by someone (Frederic?): =! for existential
equality is a bit awkward. If this has to be takes as secondary
(strong = being primary) than =e= would be preferable to me at least.

--- I think I would prefer the display notation with square brackets
for compund identifiers. Index notation may be nice in some contexts,
but in general I find it a bit too decorative (especially when piled
up...)  and hence a bit risky.

--- precedence rules: I found these a bit complicated and difficult to
follow and explain to myself. Even in your examples it took me a while
to parse correctly:

  not pre zero defined

  not a is_in {}

Even though there seems to be only one correct parsing, I feel that
perhaps some more parentheses should be forced upon the user in cases
like this... I do not quite know how this would translate to the
precedence rules.

[The correct parsing of the examples above relies on the reader
 bearing in mind the distinction between terms and formulae.  One could
 in fact force the use of further parentheses by letting grouping be
 insensitive to this distinction - rejecting axioms where the resulting
 parsing leads to formulae occurring within terms. Then one would have
 to rewrite the above examples as follows:

   not (pre zero) defined

   not (a is_in {})

 Is that OK now for atomic formulae and negation?  I hope the
 precedence rules concerning quantification and the other logical
 connectives were not also a source of confusion.  If they were: 
 my apologies - and kindly provide further illustrative examples.  
--PDM]

--- notation for datatypes: I think Frederic is right that something
like example 1.4 may be a bit confusing. Maybe really "has" instead of
">" would be better... I would stick to "=" in this context though.

--- predicate types: sorry, unlike you I prefer some non-functional
notation, so no "S*...*S->truth", please... ( pred(S*...*S) is okay).

==============================================================================
[...]

Andrzej