Prev Up Next
Go backward to B.1 Basic and Subsorted Specifications
Go up to B Abbreviated Abstract Syntax
Go forward to B.3 Architectural Specifications

B.2 Structured Specifications

  SPEC             ::= BASIC-SPEC
                     | translation SPEC RENAMING
                     | reduction SPEC RESTRICTION 
                     | union SPEC+
                     | extension SPEC+
                     | free-spec SPEC
                     | local-spec SPEC SPEC
                     | closed-spec SPEC
                     | spec-inst SPEC-NAME FIT-ARG*

  RENAMING         ::= renaming SYMB-MAP-ITEMS+

  RESTRICTION      ::= hide   SYMB-ITEMS+
                     | reveal SYMB-MAP-ITEMS+

  SPEC-DEFN        ::= spec-defn SPEC-NAME GENERICITY SPEC
  GENERICITY       ::= genericity PARAMS IMPORTS
  PARAMS           ::= params SPEC*
  IMPORTS          ::= imports SPEC*

  FIT-ARG          ::= fit-spec SPEC SYMB-MAP-ITEMS* 
                     | fit-view VIEW-NAME FIT-ARG*

  VIEW-DEFN        ::= view-defn VIEW-NAME GENERICITY VIEW-TYPE 
                                 SYMB-MAP-ITEMS*
  VIEW-TYPE        ::= view-type SPEC SPEC

  SYMB-ITEMS       ::= symb-items     SYMB-KIND SYMB+
  SYMB-MAP-ITEMS   ::= symb-map-items SYMB-KIND SYMB-OR-MAP+
  SYMB-KIND        ::= implicit | sorts | ops | preds

  SYMB             ::= ID | QUAL-OP-NAME | QUAL-PRED-NAME
  SYMB-MAP         ::= symb-map SYMB SYMB
  SYMB-OR-MAP      ::= SYMB | SYMB-MAP

  SPEC-NAME        ::= SIMPLE-ID
  VIEW-NAME        ::= SIMPLE-ID

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

CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Prev Up Next