Go backward to 1 Global Changes
Go up to Top
Go forward to Acknowledgements

2 Local Changes

Title, p. i

Replace: `22 October 1998' by: `22 July 1999'.

Insert after `available separately':

as is the list of all corrections and clarifications made since the initial release of this document in October 1998

Insert the standard `copyleft' notice:

Copyright © 1999 CoFI, The Common Framework Initiative for Algebraic Specification and Development.
Permission is granted to anyone to make or distribute verbatim copies of this document, in any medium, provided that the copyright notice and permission notice are preserved, and that the distributor grants the recipient permission for further redistribution as permitted by this notice. Modified versions may not be made.

About this document, p. viii

Remove:

Appendix F lists the main points that have been addressed since version 0.99 of this document appeared.

Contributors, p. x

Before `Erik Saaman' insert `Markus Roggenbach'.

After `Uwe Wolter' insert `Alexandre Zamulin'.

Contributors, p. xi

Replace the penultimate paragraph by:

The concrete syntax (input syntax and display format) of CASL has been designed initially by Michel Bidoit, Christine Choppy, Bernd Krieg-Brückner, and Frédéric Voisin, and coordinated by Peter D. Mosses. Feedback from the development of various prototype parsers for CASL by Hubert Baumeister, Mark van den Brand, Kolyang, Till Mossakowski, Markus Roggenbach, Axel Schairer, Christophe Tronche, Frédéric Voisin, and Bjarke Wedemeijer has also contributed significantly to the final concrete syntax design.

Ch. 1, p. 2

After `institutions' insert: `[GB92]'.

Ch. 2, p. 7

Replace:

The models of this signature and set of sentences provide

by:

This signature and the class of models over it that satisfy the set of sentences provide

cf. the first paragraph of Ch. 5.

Sect. 2.1.2.1, p. 11

After "parsing annotation" insert::

%left assoc¹

Replace the metavariable `V' by `v', for consistency with the use of lowercase metavariables for sorts, operations, and predicates. Similarly on p. 12 and in: Sect. 2.1.3.2, p. 13; Sects. 2.2.1-2, p. 17; Sect. 2.3.1, p. 18; Sect. 2.3.4.2, p. 23; and Sect. 4.1.1.3, p. 29.

Sect. 2.1.3.2, p. 13

Replace `allowed in T' by `allowed in F'.

Sect. 2.1.4.1, p. 14

Replace:

      PARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS*

by:

      PARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS+

Sect. 2.1.4.1, p. 15

Move the paragraph starting:

Note that when there is more than one alternative construct...

down to replace the sentence starting:

Some minor restrictions are imposed: In a datatype declaration...

and replace `Moreover, a' by `A'.

Sect. 2.1.4.2, p. 15

After the sentence starting:

This construct is only well-formed...

insert:

Moreover, the constructors and selectors must be distinct (as qualified symbols) from each other and from the operations declared in the local environment.

Sect. 2.1.4.2, p. 16

Continue:

(The sentences ensure that....)

with

provided that the sorts and qualified operation symbols declared by the datatype declaration are not already declared in the local environment.

Sect. 2.2.1, p. 17

At the end of the sentence starting `Note that local variable declarations' insert `instead of the optional semicolon'.

Remove the surplus spaces in ` · '. Similarly in Sect. 2.2.2, p. 17; Sect. 2.3.1, p. 18; and Sect. 8.3, p. 57.

Sect. 2.3, p. 18

Remove `(elsewhere in bold face)'.

Sect. 2.3.1, p. 18

Insert at the end:

Note that the body of a quantification extends as far as possible.

cf. clarification to App. C.2.

Sect. 2.3.3.2, p. 21

Replace:

When the predicate symbol is a constant with no argument terms, its application is simply written `PS'.

by:

When the predicate symbol is a constant p with no argument terms, its application is simply written `p'.

Similarly in Sect. 2.3.4.3, p. 23, but there using the metavariable c.

Sect. 2.3.4.3, p. 24

Replace `also written' by `written'.

Sect. 2.4, p. 25

Replace:

      TOKEN     ::= WORDS | SIGNS | DOT-WORDS

by:

      TOKEN     ::= WORDS | DOT-WORDS | SIGNS | DIGIT | QUOTED-CHAR

Replace `in Section 6.2.1' by `in Section 6.5'.

Use the fixed-width font for underscore, prime, and dot.

Replace:

      MIXFIX-ID      ::= mixfix-id TOKEN-OR-PLACE+

by:

      MIXFIX-ID      ::= TOKEN-PLACES
      TOKEN-PLACES   ::= token-places TOKEN-OR-PLACE+

Replace `list of tokens' by `list of tokens or spaces t_i'.

Replace `Braces `{...}' and square brackets `[...]' are not allowed as complete tokens in identifiers; moreover' by `Braces `{', `}' and square brackets `[', `]' are allowed as complete tokens in identifiers; however'.

Ch. 3, pp. 26-27

Replace ` < _S' by ` < ' throughout.

Remove `We may drop the subscript S when obvious from the context.'

Ch. 4, p. 28

Replace:

The models of this signature and set of sentences provide

by:

This signature and the class of models over it that satisfy the set of sentences provide

cf. the first paragraph of Ch. 5.

Sect. 4.1.1.3, p. 29

Before `It provides' insert:

The sign displayed as ` · ' may be input as `·' in ISO Latin-1, or as `.' in ASCII.

At the end, insert:

Defined subsorts may be separately related using subsort (or isomorphism) declarations--implication or equivalence between their defining formulae does not give rise to any subsort relationship between them.

Sect. 4.1.2.1, p. 30

Replace `Finally, the constructors...' by:

Finally, consider the set of qualified constructor and selector symbols declared by the free datatype: no element of this set may be in the overloading relation with any other element, nor with the qualified operation symbols from the local environment.

Sect. 4.2.1, p. 30

Replace ` < _F' by ` ~ _F', and ` < _P' by ` ~ _P'.

Ch. 5, p. 35

Append to the penultimate item:

In the case that the signature morphism does not exist, the enclosing construct is ill-formed.

In the last item, replace:

the set of all morphisms from Sigma to Sigma' that extend the given mapping, and then are identity,

by:

the unique signature morphism from Sigma to Sigma' that extends the given mapping, and then is the identity,

Append to the last item:

In the case that the signature morphism does not exist or is not unique, the enclosing construct is ill-formed.

Sect. 6.1.5, p. 40

Replace the sentence starting `Note that the specification written:' by:

Note that the specification written:
free types DD₁; ... DD_n;
is parsed as a free datatype of a basic specification, but it usually has the same interpretation as the free structured specification written:
free { types DD₁; ... DD_n; }
This equivalence holds at least in the framework for basic specifications given in Part I, under some minor restrictions: in a datatype declaration with more than one alternative, any selector that is declared as total for some alternative must be declared as a total selector with the same result sort for every other alternative; and the sorts and qualified operation symbols declared by the datatype declaration must not be already declared in the local environment.

Sect. 6.2.2, p. 43

Replace `the the' by `the'.

Replace `set of signature morphisms' by `signature morphism', also in Sect. 6.3.1, p. 45.

Replace `this set is a singleton' by `the signature morphism is defined', also in Sect. 6.3.1, p. 45.

Sect. 6.2.2, p. 44

In the paragraph starting:

Each fitting argument FA_i is regarded

replace `and the current local environment' by `(the current local environment is ignored)', cf. the minutes of the Language Design meeting in Cachan, November 1998.

Replace `The instantiation is also undefined whenever' by `The instantiation is not well-formed if'.

Replace:

and the actual parameter
SP'₁ and...and SP'_n

by:

and the union of the argument specifications
SP'₁ and...and SP'_n

Sect. 6.3.1, p. 45

After the abstract syntax grammar insert:

A view definition VIEW-DEFN with some generic parameters and some imports is written:

view
VN [SP₁] ... [SP_n] given SP"₁, ..., SP"_m : SP to SP' =
SM
end

Sect. 6.3.1, p. 46

Append:

The instantiation of a generic view with some fitting arguments is not well-formed if the instantiation of the target SP' of the view with the same fitting arguments is not well-formed.

Sect. 6.4.1, p. 47

Replace:

      TYPE       ::= OP-TYPE | PRED-TYPE | SORT

by:

      TYPE       ::= OP-TYPE | PRED-TYPE

Replace:

as determined by the local environment.

by:

as determined by the latest keyword, or, when there is none, unambiguously by the local environment.

then move the enclosing sentence down to just above the last paragraph.

Sect. 6.5, p. 48

Replace:

      COMP-TOKEN-ID  ::= comp-token-id TOKEN-ID ID+
      COMP-MIXFIX-ID ::= comp-mixfix-id TOKEN-ID ID+

by:

      COMP-TOKEN-ID  ::= comp-token-id TOKEN ID+
      COMP-MIXFIX-ID ::= comp-mixfix-id TOKEN-PLACES ID+

Replace:

A compound, token identifier COMP-TOKEN-ID or mixfix identifier COMP-MIXFIX-ID is written:
I[I₁,...,I_n]

by:

An ordinary compound identifier COMP-TOKEN-ID is written
`I[I₁,...,I_n]'; a mixfix compound identifier COMP-MIXFIX-ID is written by inserting `[I₁,...,I_n]' directly after the last token of the identifier. (Compound `invisible' identifiers without any tokens are not allowed.) Note that declaration of both compound identifiers and mixfix identifiers as operation symbols in the same local environment may give rise to ambiguity, when they involve overlapping sets of tokens.

Sect. 7, p. 52

Replace:

if two arguments have the same specification, the corresponding arguments must be identical

by:

if two arguments have the same signature, the arguments must be identical

Sect. 8.1.1, p. 54

Replace:

the type of the generic function being merely the union of the signatures of the UT_i

by:

the argument type of the generic function being merely the list of the signatures of the UT_i

Sect. 8.2, p. 55

Replace:

      UNIT-SPEC        ::= UNIT-TYPE | SPEC-NAME | ARCH-SPEC
                         | CLOSED-UNIT-SPEC

by:

      UNIT-SPEC        ::= UNIT-TYPE | SPEC-NAME | ARCH-UNIT-SPEC
                         | CLOSED-UNIT-SPEC

Remove:

      CLOSED-UNIT-SPEC ::= closed UNIT-SPEC

Sect. 8.2.2, p. 56

Replace:

An architectural specification ARCH-SPEC in a unit specification is written:

by:

      ARCH-UNIT-SPEC   ::= arch-unit-spec ARCH-SPEC
An architectural unit specification ARCH-UNIT-SPEC is written:

Sect. 8.3.1, p. 57

Replace:

where union and (non-injective) translation might introduce inconsistencies.

by:

where well-formed unions or (non-injective) translations of consistent specifications might result in inconsistencies.

Sect. 8.3.1.1, p. 58

Replace:

where the renaming R determines a mapping of symbols.

by:

where the renaming R is written `with SM', and determines a mapping of symbols, cf. Section 6.1.1.

Sect. 8.3.1.2, p. 58

Replace:

where the restriction R determines a set of symbols, and possibly a mapping of them.

by:

where the restriction R is written `hide SL' or `reveal SM', and determines a set of symbols, and in the latter case also a mapping of them, cf. Section 6.1.2.

Ch. 10, p. 62

Replace:

These are not dependent on other libraries. Then constructs for referencing distributed libraries are added.

by:

Such libraries are not dependent on other libraries. Then constructs for referencing distributed libraries are added. Finally, the form and intended interpretation of library names are explained.

Sect. 10.1, p. 63

Remove (most of it gets reinserted later):

      LIB-NAME    ::= LIB-ID | LIB-VERSION
      LIB-VERSION ::= lib-version LIB-ID VERSION
      VERSION     ::= version NUMBER+
A library identifier LIB-ID in a local library may be written as a simple identifier. A library version name LIB-VERSION in a local library is written:
LI version N₁. ... .N_n
The lists of version numbers are ordered lexicographically on the basis of the usual ordering between natural numbers.

Sect. 10.2, p. 63

Replace:

A map `IN_n ^_|-> IN_n'

by:

An identity map `IN_n ^_|-> IN_n'

Sect. 10.2, p. 64

Replace from:

When the library name LN does not include a version number,

to the end of the chapter by:

10.3 Library Names
      LIB-NAME    ::= LIB-ID | LIB-VERSION
      LIB-VERSION ::= lib-version LIB-ID VERSION
      VERSION     ::= version NUMBER+
A library name LIB-NAME without a VERSION is written simply as a library identifier LI. A library name LIB-NAME with version numbers N₁, ..., N_n is written:
LI version N₁. ... .N_n
The lists of version numbers are ordered lexicographically on the basis of the usual ordering between natural numbers.
The library name of a library definition determines how the library is to be referenced from other libraries; its interpretation as a URL determines the primary location of the library (any copies of a library are to retain the original name).
When the name of a defined library is simply a library identifier LIB-ID, it must be changed to an explicit library version LIB-VERSION before defining further versions of that library. A library identifier without an explicit version in a downloading construct always refers to the current version of the identified library: the one with the largest list of version numbers (which is not necessarily the last-created version, due to the lexicographic ordering on such lists).
      LIB-ID        ::= DIRECT-LINK | INDIRECT-LINK
      DIRECT-LINK   ::= direct-link URL
      INDIRECT-LINK ::= indirect-link PATH
A direct link to a library is simply written as the URL of the library. The location of a library is always a directory, giving access not only to the individual specifications defined by the current version of the library but also to previously-defined versions, various indexes, and perhaps other documentation.
An indirect link is written:
FI₁/.../FI_n
where each file identifier FI_i is a valid file name, as for use in a path in a URL. An indirect link is interpreted as a URL by the current global library directory.

App. A, p. A-2

In the list of symbols left unspecified insert `DIGIT, DIGITS, QUOTED-CHAR'.

App. A.1, p. A-3

Replace:

PARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS*

by:

PARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS+

App. A.1, p. A-4

Replace:

TOKEN     ::= WORDS | SIGNS | DOT-WORDS

by:

TOKEN     ::= WORDS | DOT-WORDS | SIGNS | DIGIT | QUOTED-CHAR

App. A.3, p. A-5

Replace:

TYPE       ::= OP-TYPE | PRED-TYPE | SORT

by:

TYPE       ::= OP-TYPE | PRED-TYPE

App. A.4, p. A-6

Replace:

UNIT-SPEC        ::= UNIT-TYPE | SPEC-NAME | ARCH-SPEC
                   | CLOSED-UNIT-SPEC

by:

UNIT-SPEC        ::= UNIT-TYPE | SPEC-NAME | ARCH-UNIT-SPEC
                   | CLOSED-UNIT-SPEC
ARCH-UNIT-SPEC   ::= arch-unit-spec ARCH-SPEC

App. B, p. B-1

In the list of symbols left unspecified insert `DIGIT, DIGITS, QUOTED-CHAR'.

App. B.1, p. B-2

Replace:

                   | partial-construct OP-NAME COMPONENTS*

by:

                   | partial-construct OP-NAME COMPONENTS+

App. B.1, p. B-3

Replace:

MIXFIX-ID        ::= token-places TOKEN-OR-PLACE+

by:

MIXFIX-ID        ::= TOKEN-PLACES
TOKEN-PLACES     ::= token-places TOKEN-OR-PLACE+

since TOKEN-PLACES is used in App. B.2.

Replace:

TOKEN            ::= WORDS | SIGNS | DOT-WORDS

by:

TOKEN            ::= WORDS | DOT-WORDS | SIGNS | DIGIT | QUOTED-CHAR

App. B.2, p. B-3

Replace:

TYPE       ::= OP-TYPE | PRED-TYPE | SORT

by:

TYPE       ::= OP-TYPE | PRED-TYPE

App. B.3, p. B-4

Replace:

UNIT-SPEC        ::= UNIT-TYPE | SPEC-NAME | ARCH-SPEC
                   | closed UNIT-SPEC

by:

UNIT-SPEC        ::= UNIT-TYPE | SPEC-NAME | arch-unit-spec ARCH-SPEC
                   | closed UNIT-SPEC

App. C, p. C-1

Replace:

Examples of specifications...

to the beginning of Section C.1 by:

Examples of specifications illustrating the concrete syntax are given in Appendix E. Some prototype parsers for CASL have been implemented (see the CoFI Tools task group web page).

App. C.1, p. C-2

Replace

Appendix A--mainly just by replacing the prefix constructors of the latter by mixfix constructors. Section C.3 explains various precedence rules for disambiguation.

by:

Appendix B, except for the productions for mixfix formulae and terms. The context-free grammar is ambiguous; Section C.3 explains various precedence rules for disambiguation, and the intended grouping of mixfix formulae and terms.

Append:

Finally, Section C.6 introduces several annotations used to provide literal syntax for numbers, strings, and lists.

App. C.2, p. C-2

Append:

The following nonterminal symbols are for lexical syntax, and defined in Section C.4: WORDS, DOT-WORDS, NO-BRACKET-SIGNS, DIGIT, DIGITS, NUMBER, QUOTED-CHAR, URL, and PATH. Lexical analysis for CASL is generally independent of the context-free parsing (apart from the recognition of NUMBER, URL, and PATH, which may appear in libraries but not within individual specifications).
Context-free parsing of CASL specifications according to the grammar in this section yields a parse tree where terms and formulae occurring in axioms and definitions have been grouped with respect to explicit parentheses and brackets, but where the intended applicative structure has not yet been recognized. A further phase of mixfix grouping analysis is needed, dependent on the symbols declared in the specification and parsing annotations, before the parse tree can be mapped to a complete abstract syntax tree.

App. C.2.1, p. C-4

Replace:

                  | PRED-SYMB
                  | PRED-SYMB ( TERMS )
                  | TERM TERM...TERM

by:

                  | MIXFIX...MIXFIX

and move to the end of the enclosing production.

Replace:

PRED-SYMB       ::= PRED-NAME  |  ( pred PRED-NAME : PRED-TYPE )

by:

QUAL-PRED-NAME  ::= ( pred PRED-NAME : PRED-TYPE )

Replace:

TERM            ::= SIMPLE-TERM...SIMPLE-TERM

SIMPLE-TERM     ::= ID
                  | ( var VAR : SORT )
                  | ( op QUAL-OP-NAME )
                  | OP-SYMB ( TERMS )
                  | SIMPLE-TERM : SORT
                  | SIMPLE-TERM as SORT
                  | TERM when FORMULA else TERM
                  | ( TERM )

OP-SYMB         ::= OP-NAME  |  ( op OP-NAME : OP-TYPE )

by:

TERM            ::= MIXFIX...MIXFIX | LITERAL

MIXFIX          ::= WORDS | DOT-WORDS | NO-BRACKETS | PLACE
                  | QUAL-VAR-NAME | QUAL-OP-NAME | QUAL-PRED-NAME
                  | MIXFIX : SORT
                  | MIXFIX as SORT
                  | MIXFIX when FORMULA else MIXFIX
                  | ( TERMS )
                  | [ TERMS ] | [ ]
                  | { TERMS } | { }

QUAL-VAR-NAME   ::= ( var VAR : SORT )

QUAL-OP-NAME    ::= ( op OP-NAME : OP-TYPE )

Replace:

MIXFIX-ID       ::= TOKEN-OR-PLACE...TOKEN-OR-PLACE
TOKEN-OR-PLACE  ::= TOKEN | PLACE
TOKEN           ::= WORDS | SIGNS | DOT-WORDS

by:

MIXFIX-ID       ::= TOKEN-ID PLACE-TOKEN-ID ... PLACE-TOKEN-ID
                  |          PLACE-TOKEN-ID ... PLACE-TOKEN-ID
PLACE-TOKEN-ID  ::= PLACE TOKEN-ID
                  | PLACE
TOKEN           ::= WORDS | SIGNS | DOT-WORDS | DIGIT | QUOTED-CHAR

App. C.2.2, p. C-5

Replace:

SOME-IMPORTS    ::= given SPEC-NAME ,..., SPEC-NAME

by:

SOME-IMPORTS    ::= given GROUPED-SPEC ,..., GROUPED-SPEC

Replace:

VIEW-TYPE       ::= GROUP-SPEC -> GROUP-SPEC

by:

VIEW-TYPE       ::= GROUP-SPEC to GROUP-SPEC

Replace:

TOKEN-ID        ::= ... | TOKEN [ ID ,..., ID ]
MIXFIX-ID       ::= ... | TOKEN-PLACES [ ID ,..., ID ]

by:

TOKEN-ID        ::= ... | TOKEN [ ID ,..., ID ]

App. C.3, p. C-7

Replace:

The grammar for input syntax is quite ambiguous. This section provides some precedence rules for disambiguation. Note that the syntax for atomic formulae and terms caters for use of mixfix notation when applying predicates and operations; however, the recognition of the exact applicative structure of these constructs is left unspecified here, since it is inherently context-dependent.

by:

The context-free grammar given in Section C.2 for input syntax is quite ambiguous. This section explains various precedence rules for disambiguation, and the intended grouping of mixfix formulae and terms (which is to be recognized in a separate phrase, dependent on the declared symbols and parsing annotations).
C.3.1 Precedence

At the end of the item concerning the precedence of quantifications, insert:

Moreover, a quantification may be used on the right of a logical connective without grouping parentheses, e.g.,
`F <=> exists x:s . G <=> H' is parsed as
`F <=> (exists x:s . G <=> H)'.

At the beginning of the next paragraph, after `The declaration' insert as a footnote:

Declarations occurring anywhere in the enclosing list of basic items are taken into account when disambiguating the grouping of symbols in a term.

At the end of the last paragraph in the section, insert:

Parsing annotations may even override the rules given above for the relative precedence of postfix, prefix, and infix symbols.

Append:

C.3.2 Mixfix Grouping Analysis
Note that ID is not an alternative of MIXFIX, since the notation for compound identifiers could be confused with mixfix notation involving square brackets.
Mixfix grouping analysis of a specification should be equivalent to context-free parsing according to a derived grammar--obtained from the grammar in Section C.2 by replacing the alternatives involving MIXFIX with alternatives determined (partly) by the declared symbols, as follows:
FORMULA ::= ... | QUAL-PRED-NAME
          | QUAL-PRED-NAME ( TERMS )

TERM    ::= ... | QUAL-VAR-NAME | QUAL-OP-NAME
          | QUAL-OP-NAME ( TERMS )
          | TERM : SORT
          | TERM as SORT
          | TERM when FORMULA else TERM
          | ( TERM )
plus
TERM    ::= ... | id
for each declared variable or constant name id, plus
TERM    ::= id ( TERMS )
for each declared operation symbol id of positive arity, plus
TERM    ::= t₁ TERM t₂ ... TERM t_n
for each declared mixfix operation symbol t₁ __ t₂ ... __ t_n (with t₁ and t_n possibly empty), plus
FORMULA   ::= ... | id
for each declared predicate constant name id, plus
FORMULA   ::= id ( TERMS )
for each declared predicate symbol id of positive arity, plus
FORMULA   ::= t₁ TERM t₂ ... TERM t_n
for each declared mixfix predicate symbol t₁ __ t₂ ... __ t_n (with t₁ and t_n possibly empty).
It would be possible to obtain a fixed grammar for a sub-language of CASL lacking mixfix notation in a similar way, using the appropriate kinds of ID in place of the declared ids above. (It may be convenient to obtain all these various grammars as extensions of a root grammar that is completely uncommitted about the notation used for applications, etc.)

App. C.4, p. C-9

Replace the entire section by:

This section defines the lexical syntax of WORDS, DOT-WORDS, NO-BRACKET- SIGNS, DIGIT, DIGITS, NUMBER, and QUOTED-CHAR, which are used in Section C.2, together with that of FRACTION, FLOATING, and STRING, which are used in Section C.6. The lexical syntax of URL and PATH has not yet been finalized, and is left open.
Spaces and other layout characters terminate lexical symbols (except for QUOTED-CHAR and STRING) and are otherwise ignored. The next lexical symbol recognized is as long as possible.
WORDS        ::= WORD _..._ WORD

DOT-WORDS    ::= . WORDS

WORD         ::= LETTER-P-D ... LETTER-P-D
LETTER-P-D   ::= LETTER | "'" | DIGIT
LETTER       ::= A | B | C | D | E | F | G | H | I | J | K | L | M 
               | N | O | P | Q | R | S | T | U | V | W | X | Y | Z 
               | a | b | c | d | e | f | g | h | i | j | k | l | m 
               | n | o | p | q | r | s | t | u | v | w | x | y | z 
               | À | Á | Â | Ã | Ä | Å | Æ | Ç | È | É | Ê | Ë | Ì 
               | Í | Î | Ï | Ñ | Ò | Ó | Ô | Õ | Ö | Ø | Ù | Ú | Û 
               | Ü | Ý | ß | à | á | â | ã | ä | å | æ | ç | è | é 
               | ê | ë | ì | í | î | ï | ñ | ò | ó | ô | õ | ö | ø 
               | ù | ú | û | ü | ý | ÿ 
DIGIT        ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

DIGITS       ::= DIGIT DIGIT ... DIGIT

NUMBER       ::= DIGIT | DIGITS
A WORDS must start with a LETTER, and must not be one of the reserved keywords used in the context-free syntax in Section C.2. The (51) keywords are:
and arch as assoc axiom axioms closed comm def else end exists 
false fit forall free from generated get given hide idem if in 
lambda library local not op ops pred preds result reveal 
sort sorts spec then to true type types unit units 
var vars version view when with within .
LETTER includes all the ISO Latin-1 national and accented letters except for the Icelandic `eth' and `thorn'.
NO-BRACKET-SIGNS ::= NO-BRACKET-SIGN ... NO-BRACKET-SIGN
A NO-BRACKET-SIGNS must not be one of the following reserved symbols:
:  :?  ::=  =  =>  <=>  .  ·  |  |->  \/  /\ ¬ 
These sequences of characters may however be used together with other characters in a NO-BRACKET-SIGNS. For example, `==', `:=', and `||' is each recognized as a complete NO-BRACKET-SIGNS. Note that identifiers that start or finish with a NO-BRACKET-SIGNS need to be separated by (e.g.) a space from adjacent reserved symbols: a sequence of characters such as ` #: ' is always recognized as a single symbol, whereas ` # : ' is recognized as two symbols.
Despite its use in the context-free syntax as a terminal symbol, a single character `<', `*', `?', `!', or `/' is also recognized as a complete NO-BRACKET-SIGNS. The ISO Latin-1 characters for product `×', negation `¬ ', and raised dot `·' are recognized as alternatives for the terminal symbols `*', `not', and `.', respectively.
NO-BRACKET-SIGN  ::= + | - | * | / | \ | & | = | < | >
                   | ! | ? | : | . | $ | @ | # | ^ | ~
                   | !` | ?` | × | ÷ | £ | © | ± | ¶ | §
                   | ¹ | ² | ³ | · | ¢ | ° | ¬  | µ | "|"
Note that NO-BRACKET-SIGN does not include the following ASCII signs:
( ) [ ] { } ; , ` " %
nor the ISO Latin-1 signs for general currency, yen, broken vertical bar, registered trade mark, masculine and feminine ordinals, left and right angle quotes, fractions, soft hyphen, acute accent, cedilla, macron, and umlaut.
QUOTED-CHAR ::= "'" CHAR "'"

CHAR        ::= " " | ! | '\"' | # | $ | ... 
              | "\'" | ... | "\\" | ...
              | \n | \t | \r | ...
              | \000 ... | \255

FRACTION    ::= NUMBER . NUMBER

FLOATING    ::= NUMBER "E" OPT-SIGN NUMBER
              | FRACTION "E" OPT-SIGN NUMBER
OPT-SIGN    ::= + | - | 

STRING      ::= '"' '"'
              | '"' CHAR ... CHAR '"'
Pairs of single quotes `'...'' (with no spaces between them) are used in the above productions to indicate symbols containing the double quote character `"', and vice versa.

App. C.5, p. C-10

After `Comments may be inserted anywhere' insert as a footnote:

It is unclear how to cope with the possibility of comments occurring everywhere using standard parser-generators, when the comments are not to be discarded by attached to abstract syntax trees. Should the positions where comments may occur be (severely) restricted, as foreseen for annotations? See the Tools Note T-7 [Sch99] with further analysis of the problem and for a report on how it has been solved in the INKA front end.

App. C.5.1, p. C-11

Replace:

Further details concerning the use of formatting instructions in comments are given in [BCKB+98].

by:

Text that is `commented-out' in a CASL specification is indicated by a comment of the form `%(...%)'; it is not shown at all in the display format. Note that comments introduced by `%%' may occur within `%(...%)', and vice versa; but further nesting of comments is not possible.
The body of comment is generally input as plain (ISO Latin-1) text. CASL syntax within comments is indicated by `<CASL>... </CASL>' (each line still starting with `%%'); such syntax is parsed and displayed as usual, but with each line in its display prefixed by `%%'. (The `<...>...</...>' notation for delimiting constructs comes from SGML and HTML; the `/' in the closing delimiter may be read suggestively as "over".)
Instructions to formatters can be embedded in comments in the same way as CASL syntax, using the name of the formatting language instead of `CASL' in the delimiters `<CASL>...</CASL>'. Thus for LaTeX, one uses `<latex>...</latex>'; other envisaged formatters are for HTML and RTF. Each formatter ignores the instructions for the alternative formatters.
Formatting languages cannot be nested: the start of a new language implies the end of the current one. The name of the language may be omitted in the terminator, if desired, writing merely `</>'. The end of a comment implicitly terminates the current language.
Typically, one may want to specify special instructions for one or more particular formatters, leaving all other formatters to display some plain text as best they can; this may be written e.g. `<latex>...<html>...<other>...</>', thus:
... %% This is a fancy comment using <latex>\LaTeX<other>LaTeX</>
    %% and continuing with plain text

App. C.5.2.1, p. C-11

Replace by:

A label annotation is of the form `%[ID,...,ID]' or `%[NNUMBER]'. It may be written immediately before a FORMULA in a BASIC-ITEMS construct, and immediately before an ALTERNATIVE in a DATATYPE-DECL.

App. C.5.2.2, p. C-12

Replace:

Further details concerning the use of formatting instructions in annotations are given in [BCKB+98].

by:

An explicit `<other>' part can be used to provide abbreviations, e.g.,
... VLSI %!<other>Very_Long_Simple_Identifier%!
The input symbol whose display is to be affected may also be indicated explicitly in the display annotation, which may then be inserted at any point in a CASL specification, e.g.,
... %! div<latex>$\div$<html>&divide;%!
(The space following the opening `%!' is optional, except when the input symbol starts with a `<'.)
The notation for display annotations with implicit input symbols could be made more concise by letting <latex> be implied by an initial `$' or `\', and <html> be implied by an initial `&'. E.g.,
... div %!$\div$ &divide;%!
Note that readability is not a crucial issue here, since display annotations are not themselves to be displayed, and can be seen only when using an editor on the input syntax.
Finally, display annotations generalize to formatting mixfix notation by interpreting the place-holder `__' as such in the formatting instructions, e.g.,
... sum__to__ %!<latex>\sum_{__}^{__}<html>SUM<sub>__<sup>__%!
This indicates the display not only for the mixfix operation symbol per se, but also for its application to argument terms (the place-holders being replaced by the arguments in the same order as input). If needed, LaTeX-style notation for argument positions `#n' could be provided too.

App. C.5.2.3, p. C-12

Replace:

An approved set of parsing annotations and their syntax have not yet been worked out.

by:

A set of parsing annotations has been proposed in Note L-11 [RM99] (see also Note T-6 [Mos98a]). The following have been approved:
Annotations on Operator Precedences: The proposal was accepted with the amendment that operator lists of more than one item are to be grouped by {...}..
Annotations on Associativity: `%left assoc' and `%right assoc' were both accepted.
These annotations, applicable to an entire library, are to allow users to specify the precedence of operation symbols, and the significance of layout in the so-called "offside" rule. Their primary purpose is to allow the omission of grouping parentheses and/or list separators in the input; but formatters may also exploit them to avoid superfluous parentheses in the display.
A prededence annotation is written:
%prec {id₁, ..., id_n} < {id_n+1, ..., id_n+k}
Here each id_i is an (unqualified) mixfix operation symbol of the form `__ ... __ ... __'. The relation specifies that for 1 < i < n the symbol id_i has lower priority (i.e., binds weaker) than the symbol id_j, where n+1 < j < n+k. In case that there is just one operation symbol, the grouping braces may be omitted.
It is also possible to specify that two mixfix operation symbols id₁ and id₂ (which need not to be of form `__ ... __ ... __') are not allowed to be combined without explicit grouping parentheses This is done using an annotation:
%prec {id₁, ..., id_n} <> {id_n+1, ..., id_n+k}
In case that there is just one operation symbol, the grouping braces may be omitted.
The precedence annotations determine a pre-order, which is obtained in the following way:
Expand all precedence relations into binary relations, i.e. from annotations of the form {id₁, ..., id_n} < {id_n+1, ..., id_n+k} we get { (id_i, id_j) | 1 < i < n, n+1 < j < n+k }, and from annotations of the form {id₁, ..., id_n} <> {id_n+1, ..., id_n+k} we get { (id_i, id_j), (id_j, id_i) | 1 < i < n, n+1 < j < n+k }.
Take the union of all declared expanded precedence relations with the predefined precedences listed in Section C.3.
Take the reflexive transitive closure of this union.

If two symbols occurring in a term of atomic formula are equivalent (i.e. related in both directions) or incomparable (i.e. related in no direction) in the precedence relation, their grouping has to be explicitly specified by using parentheses.
There are two associativity annotations, `%left assoc' and `%right assoc'. They may be used immediately after an operation or predicate declaration. For example, declaring __+__ to be left associative means that t₁ + t₂ + t₃ is parsed as (t₁ + t₂) + t₃, while declaring it to be right associative leads to t₁ + (t₂ + t₃). If there is no associativity annotation for a mixfix symbol, it is not allowed to repeat that symbol without explicit grouping using parentheses.
For precedence and associativity annotations, we adopt non-linear visibility, that is, they are visible in the whole enclosing basic specification (cf. Section C.3).
Precedence annotations interact with structured specifications in the same way as the subsorting relation. That is, for renamings and restrictions, the precedence relation is lifted along the renaming or restriction. For unions and extensions, the precedence relations are united. Note that in the case that there are conflicting precedence annotations this may lead to equivalent symbols in the union. In this case these symbols cannot be combined without explicit grouping. Associativity annotations are translated along renamings and restrictions and united along unions and extensions in the same way as the operations they refer to.

App. C.5.2.4, p. C-12

Replace:

A set of semantic annotations has been proposed, but not yet decided.

by:

A set of semantic annotations has been proposed in Note L-11 [RM99]. The following have been approved:
The annotation `%cons' was accepted with the following two supplements on its description in Note L-11: the annotation is left associative; and the annotation may not be used in case of an import.
An annotation `%imply' was considered as a desirable alternative to `%cons', and is being considered further.
The annotation `%def' was accepted. Note that if the syntax is of a restricted form, then tools can statically prove the associated proof obligation, e.g. as in the the HOL proof system.
These annotations are used to express known (or presumed) features of the semantics of the specification, e.g., that an extension is `conservative', or that certain formulae are consequences of the specification.
The annotation `%cons' may immediately follow either:
a `then' keyword within an EXTENSION, in which case, let SP be the part of the EXTENSION just up to, but excluding the annotated `then', and let SP' be the specification immediately following the `then'; or
the equals sign within a SPEC-DEFN, in which case, let SP be the union of the imports, extended by the union of the parameters, and let SP' be the body of the specification definition.
The annotation expresses that SP' is a conservative extension of SP, i.e. all SP-sentences that follow from (SP then SP') already follow from SP alone.
The annotation `%def' may occur at the same places as the annotation `%cons'. It expresses that SP' is a definitional extension of SP, i.e. each model of SP can be uniquely extended to a model of (SP then SP') (this implies a bijective correspondence between the two model classes). Note that `%def' is strictly stronger than the `%cons' annotation.
An annotation `%implies' that allows to specify the intended consequences of a specification is being considered.

Append:

C.6 Syntax for Literals
In this section, several annotations for operations are introduced that can be used to provide a literal syntax for numbers, strings and lists. These annotations can occur just after a SIG-ITEM.
C.6.1 Literal syntax for numbers
LITERAL ::= NNUMBER
The annotation for declaring an operation to be used for concatenation of digits within a number is written `%number f'. Only one such annotation within a specification SPEC is allowed, and f must have been declared as a binary operation.
The annotation has the effect that an NNUMBER of the form d₁ ...d_n (where n>1 and each d_i is a DIGIT) is translated to the (abstract syntax of) the term f(f(...f(t₁,t₂) ...,t_n-1),t_n), where t_i is the abstract syntax tree for d_i.
Vice versa, an abstract syntax tree corresponding to a term of the above form which is maximal (i.e., it is not a subterm of a larger term of the same form) is expected to be printed as d₁ ...d_n.
If there is no `%number' annotation, then an NNUMBER is not recognized as a well-formed LITERAL.
LITERAL ::= ... | FRACTION | FLOATING
The annotation for declaring the operations used for evaluating the decimal point and the exponentiation `E' within FRACTION or a FLOATING is written `%floating f g'. Only one such annotation within a specification SPEC is allowed, and f and g must have been declared as binary operations.
The annotation has the effect that a FRACTION of the form n₁.n₂ (where each n_i is a NUMBER) is translated to the (abstract syntax of) the term f(t₁,t₂), where t_i is the abstract syntax tree for n_i, i=1,2.
Similarly, a FLOATING of the form `n₁En₂' (where n₁ is a NUMBER or a FRACTION and n₂ is of form OPT-SIGN NUMBER) is translated to the (abstract syntax of) the term g(t₁,t₂), where t_i is the abstract syntax tree for n_i, i=1,2.
Vice versa, an abstract syntax tree corresponding to a term of one the above forms which is maximal (i.e., it is not a subterm of a larger term of the same form) is expected to be printed as n₁.n₂ or n₁ E n₂, respectively.
If there is no `%floating' annotation, then neither a FRACTION nor a FLOATING is recognized as a well-formed LITERAL.
C.6.2 Literal syntax for strings
LITERAL ::= ... | STRING
The annotation for declaring an operations for the empty string and for concatenation of a character with a string is written `%string c f'. Only one such annotation within a specification SPEC is allowed, and c must have been declared as a constant, while f must have been declared as a binary operation.
The annotation has the effect that an STRING of the form `"c₁ ...c_n"' (where n > 0 and each c_i is a CHAR) is translated to the (abstract syntax of) the term f(t₁,f(t₂, ...f(t_n,c)...)), where t_i is the abstract syntax tree for the QUOTED-CHAR `'c_i''.
Vice versa, an abstract syntax tree corresponding to a term of the above form which is maximal (i.e., it is not a subterm of a larger term of the same form) is expected to be printed as `"c₁ ...c_n"'.
If there is no `%string' annotation, then a STRING is not recognized as a well-formed LITERAL.
C.6.3 Literal syntax for lists
The annotation for declaring a list-like syntax is written `%list b₁ __ b₂ c f'. b₁ and b₂ are SIGNS, c must have been declared as a constant, while f must have been declared as a binary operation.
The attribute leads to an extension of the syntax for LITERALs:
LITERAL ::= ... | b1 b2
                | b1 TERM , ... , TERM b2
A list of the form `b₁ t₁,...,t_n b₂' (where n > 0 and each t_i is a TERM) is translated to the (abstract syntax of) the term f(u₁,f(u₂, ...f(u_n,c)...)), where u_i is the abstract syntax tree for c_i.
Vice versa, an abstract syntax tree corresponding to a term of the above form which is maximal (i.e., it is not a subterm of a larger term of the same form) is expected to be printed as `b₁ t₁,...,t_n b₂'.

App. D: Display Format

Replace:

This appendix is from the original documents presenting the CASL concrete syntax design proposal [BCKB+98].
It indicates how each input symbol might be displayed when formatted for printing using LaTeX. (Some mathematical symbols are simply displayed as the corresponding input symbols in this HTML version.)

by:

This appendix indicates how each input symbol is to be displayed when formatted for printing using LaTeX, as well as for web browsing using HTML. A LaTeXpackage implementing this display format is available [Mos98b].

App. D.1, p. D-1

Replace:

Moreover, characters whose display format is in ISO Latin-1 may always be used for input. This allows the direct input of the symbols displayed as `¬ ', `×', and ` · ',

by:

Moreover, characters whose display format is in ISO Latin-1 may be used for input. This allows the direct input of the symbols displayed as `¬ ' and `×' (also the bullet sign may be input as a raised dot),

App. D.2, p. D-1

Replace by:

Only keywords that indicate specification structure are displayed boldface; all keywords occurring in a FORMULA, an ATTRIBUTE, or an ALTERNATIVE are displayed in the same italic font as identifiers.

spec
Add_Num_Efficiently =
sort
Num
ops
0,1 : Num;
__0, __1 : Num -> Num;
__+__ , __ ++ __ : Num×Num -> Num

by:

spec
Add_Num_Efficiently =
generated type
Num ::= 0 | 1 | __0(Num) | __1(Num)
ops
__+__ , __ ++ __ : Num×Num -> Num

App. E.3.5, p. E-9

Replace the definitions of Implement_Succ_by_Plus and
Efficient_Add_Num (which were incorrect) by:

arch spec
Efficient_Add_Num =
units

N:Add_Num_Efficiently;
M:{ op succ(n:Num):Num = n+1 } given N
result
M hide 1, __0,__1,__ ++ __
end

App. F, pp. F-1, F-2

Remove altogether.

CoFI Document: CASL/Summary-Changes -- Version: 1.0 -- 22 July 1999.
Comments to cofi-language@brics.dk