Appendix A: Remaining Issues for Discussion

Parsing annotations:

The range of desired parsing annotations needs to be clarified. Candidates include relative/absolute precedence in terms, and the offside rule concerning layout.

Precedence in formulae:

The current relative precedence rules for logical connectives have been in the proposal since its first public version in September 1997. The question has now been raised as to whether conjunction should perhaps be given higher precedence than disjunction, and whether iterated implications should be allowed (then associating to the right).

Although these conventions are widely adopted in texts on formal logic, and in some other specification languages, the majority of the authors of the original proposal felt that the dangers of misinterpretation by those relatively untrained in formal logic outweighed the benefits of omitting the occasional pair of parentheses. Moreover, mixtures of conjunction and disjunction, and nested implications, seem to be used rather infrequently in practice.

Unless further arguments are advanced, the precedence of the logical connectives will remain as it is now. However, there may still be a possibility of using parsing annotations to allow the omission of grouping parentheses in formulae as well as in terms.

Keywords for translation etc.:

The keywords ending with `ing' (`hiding', `renaming', `revealing', `fitting') have been replaced by the corresponding imperative forms, following an (admittedly rather late) suggestion by one of the authors of this document. If objections arise, the concrete syntax may quickly revert to the `ing' forms.

Views (named morphisms):

No concrete syntax has yet been proposed for the definition and use of views.

Architectural specifications:

The current proposal is new--it needs illustrative examples and public discussion before any decision is taken.

Libraries:

The current proposal is new, but rather straightforward and perhaps uncontroversial? Note that the abstract syntax of VERSION has not yet been decided.