Appendix B: Previous Issues for Discussion

The conclusions from the (exhausting!) discussions so far are indicated like this below.

Keyword for datatype declarations:

Since it is agreed that these can no longer be mixed with sort declarations, a new initial keyword is needed. The current proposal is `type'. Those who object to `type' should indicate what other keyword they would prefer. --No objections were raised.

Precedence in terms and mixfix notation:

Parsers and formatters for CASL may be allowed to take account of precedence annotations and other annotations concerned with the omission of grouping parentheses, such as the "offside" rule. It seems to provide an unobtrusive way to allow the exploitation of syntactically-sophisticated tools, without jeopardizing the interchange of CASL specifications. The remaining issue here is the degree of mixfix notation (and built-in precedence) that should be provided as default, in the absence of explicit annotations. --Since anonymous operations used in first-order CASL specification can be renamed when referenced from higher-order specifications, there appear to be no conclusive grounds for restricting the generality of mixfix notation. However, this decision may be revised if implementation of the parsing of full mixfix notation proves to be impractical.

Optional terminators:

It has not yet been determined whether allowing optional semicolons at the end of semicolon-separated lists, (as indicated in the current proposal by the meta-notation `;/ ') is possible in LALR(1) and LL(2) languages. If it turns out that it is not possible, there is the choice between always or never terminating such lists with semicolons. --It appears that both LALR(1) and LL(2) parsers can indeed deal with optional semicolons! (Otherwise, it would have been preferred always to require terminating semicolons.)

The current proposal allows an optional `end' at the end of a specification definition. Here, it seems that there is no look-ahead problem: it is simply a matter of the readability of a sequence of specifications in a library. Should the `end' be rather required, or forbidden? --It is left optional.

Syntax for imports in generic specifications:

To avoid a nasty ambiguity (it is unclear whether PAR1 is an argument of SP or a parameter of S in `spec S imports SP [PAR1] [PAR2] = ...') the PARAMS have been put before the IMPORTS. --This has been accepted.

December 1997:

Datatype declarations:

A last-minute change has been made here! The usefulness of partial constructor functions, and for explicit indication of whether selectors are total or partial, was realized very recently, and has only been briefly discussed between some of the authors of this proposal. The coordinator was encouraged to make such a change at this late stage partly because this had the benefit of eliminating several other outstanding issues. Indicating totality or partiality of constructors and selectors requires an extra component in the abstract syntax--but this then simplifies the intended semantics, it seems, as well as providing extra generality. --This change has now been agreed. Note that partial constructors are not useful in a `free datatype' declaration, since they would then be totally undefined.

Operation declarations and predicate types:

Acceptable alternatives to the `pred(...)' notation for predicate types have not been found.¹

The use of `pred' in predicate types, however, seems to rule out the possibility of replacing the keyword `op' by `fun' and `pred', which at least one of the authors would like to see (despite the fact that the use of `op' was agreed at the meeting in Amsterdam). --It has been agreed to use `pred' to start a list of predicate declarations that merely list the argument sorts, relying on the context to avoid misinterpretation as declaration of product values.

Function declarations and attributes:

No agreement for making the concrete syntax of attributes look like higher-order axioms has been reached--nor have examples of practical examples that exploit the extra generality of separating attributes from declarations been found. The coordinator has therefore chosen to adopt the conservative proposal of listing attributes in function declarations, essentially as in OBJ3. However, since functions may be redeclared in CASL, it is still possible to introduce attributes for previously-declared functions in an extension specification. --The proposal has been accepted.

Existential equations:

Is the proposed input syntax `T=.=T', displaying as `T=.=T', acceptable? Previous proposals have included `T=e=T' and `T=d=T' (which is more mnemonic of definedness'²). Admittedly this use of `T=.=T' is unconventional, and there is also the problem that readers may not notice the raised dot at all, unless it is made bolder. Anyway, this is an isolated issue, and the symbol to use here can be changed without much bother if a consensus can be found for that. The present proposal seems at least to be aesthetically pleasing. --The display of `T=.=T' as `T=.=T' was rejected, and we agreed to revert to `T=e=T', displaying (when possible) as ` =^e '.

Precedence in terms and mixfix notation:

The acceptance of ungrouped iterations such as `a+b+c' now depends on the declaration of the associativity attribute for (supersorts of) the sorts of the arguments. It needs to be clarified whether this gives significant difficulties for the implementation of parsers. --It appears that parsers may initially group (e.g.) to the left, and leave rejection of iterations of non-associative operations to later, provided that explicit grouping parentheses are recorded somehow in the parse tree.

October 1997:

Datatype declarations:

Is the use of `=' both here and in ISO-DECL too confusing, and if so, which syntax should be changed, and to what? Should there be a more concise syntax for the freely-generated case, which may occur quite frequently, and if so, what should it be? --The equality sign is no longer proposed for use in datatype declarations.

Function attributes:

Is the proposed notation adequate? Could one find a satisfactory notation more suggestive of instantiation, or application of a higher-order predicate to the function(s)? Should the use of uppercase letters be allowed/required in attributes such as aci? Should some of the lesser-used combinations of attributes be removed, and if so, which? --2-4 letter abbreviations for combinations of attributes are no longer proposed.

Predicate types:

A syntax such as `S*...*S->truth' was (briefly) discussed in Amsterdam; would it be preferable to the `pred(S*...*S)' syntax? Note that it could then be used in PRED-DEFN to indicate the `result type' of the application. --This idea found little support, and has been dropped.

Existential equations:

Using a question mark to decorate the equality sign would be rather misleading here, in view of its use elsewhere in the proposal to indicate the possiblity of undefinedness. Previous proposals included T=e=T, displaying as T =^e T; would that, or perhaps some other syntax altogether, be preferable to the proposed T=!T notation? --The `e', although conventional, is not sufficiently suggestive of `definedness', and the notation T=d=T was then proposed instead.

Mixfix notation:

How general should this be? Should it be only prefix, postfix, and infix, or more general patterns of argument place-holders? Should `invisible' symbols such as `__ __' be allowed? --Full mixfix notation is allowed, but not all CASL parsers need support mixfix notation.

Precedence in terms:

The proposal is to give all infixes uniformly the same precedence, lower than that of all prefixes, which is in turn lower than that of all postfixes. (The terminology infix, prefix and postfix can be generalized to take account of mixfix symbols with arbitrary patterns of place-holders.) Should users rather specify explicit (relative or absolute) precedence for each operator? Should there be fixed precedence for symbols starting with particular characters? --Further precedence rules could be provided using annotations, but not all CASL parsers need take account of them.

Compound identifiers:

The proposed input syntax with square brackets is the same as in LSL (see the CoFI Catalogue). Should it be displayed in the same way, rather than as the proposed subscripts? Or should ordinary parentheses be used for input and display? --The square brackets are now displayed as input, without subscripts. In either case, should the notation for compound identifiers be used also for parameter lists and instantiation of generic specifications?

September 1997:

Mixing verbose and concise styles;

The desirability of this might be questioned--perhaps it should always be possible for users to configure parsers and formatters, to determine the preferred combination of alternatives? --The differences between the verbose and concise styles have been eliminated.

Keywords:

Should singular forms of the plural keywords be allowed? --Yes! Should upper- and/or mixed-case letters be allowed? --No! Should other abbreviations be allowed, e.g., assoc for associative? --The longer full words have been eliminated.

Freely-generated datatype declarations:

Consideration of concrete syntax for this construct is currently deferred until concrete syntax for structuring constructs has been clarified. Should it rather be incorporated straight away? --Yes! but reconsidered later as well...

Function definitions:

The proposed concrete syntax resembles function definitions in programming languages such as Pascal and Ada: the type of each argument and result is given, rather than the complete function type. Is this clear enough? --Yes! Will it generalize sensibly to higher-order function definitions in extensions of CASL? --Hopefully...

Qualified function and predicate symbols:

Should one use e.g. quotation marks rather than the proposed parentheses for grouping the name and type in an application? --No!

HTML display:

Some of the mathematical signs used in the concise display format are not available in HTML, and they have been either approximated or replaced by the verbose display format in the HTML version of this document. Are better approximations available? --Approximations are no longer used: the input syntax is shown when the mathematical sign for the display format is unavailable. Should one perhaps always use the verbose display style in HTML? --This is no longer an option.