Prev Up Next
Go backward to C.2.1 Basic Specifications with Subsorts
Go up to C.2 Context-Free Syntax
Go forward to C.2.3 Architectural Specifications

C.2.2 Structured Specifications

  SPEC            ::= BASIC-SPEC 
                    | SPEC RENAMING
                    | SPEC RESTRICTION
                    | SPEC and SPEC and...and SPEC
                    | SPEC then SPEC then...then SPEC
                    | free GROUP-SPEC
                    | local SPEC within SPEC
                    | closed GROUP-SPEC
                    | GROUP-SPEC
! GROUP-SPEC      ::= { SPEC }
                    | SPEC-NAME
                    | SPEC-NAME [ FIT-ARG ]...[ FIT-ARG ]

  RENAMING        ::= with SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS

  RESTRICTION     ::= hide SYMB-ITEMS ,..., SYMB-ITEMS
                    | reveal SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS

  SPEC-DEFN       ::= spec SPEC-NAME = SPEC end/
                    | spec SPEC-NAME SOME-GENERICS = SPEC end/
  SOME-GENERICS   ::= SOME-PARAMS | SOME-PARAMS SOME-IMPORTS
  SOME-PARAMS     ::= [ SPEC ]...[ SPEC ]
  SOME-IMPORTS    ::= given SPEC-NAME ,..., SPEC-NAME

  FIT-ARG         ::= SPEC fit SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS
                    | SPEC
                    | view VIEW-NAME 
                    | view VIEW-NAME [ FIT-ARG ]...[ FIT-ARG ]

  VIEW-DEFN       ::= view VIEW-NAME : VIEW-TYPE end/
                    | view VIEW-NAME : VIEW-TYPE = 
                           SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS end/
                    | view VIEW-NAME SOME-GENERICS : VIEW-TYPE end/
                    | view VIEW-NAME SOME-GENERICS : VIEW-TYPE = 
                           SYMB-MAP-ITEMS ,..., SYMB-MAP-ITEMS end/
! VIEW-TYPE       ::= GROUP-SPEC -> GROUP-SPEC

  SYMB-ITEMS      ::= SYMB
                    | SOME-SYMB-KIND SYMB ,..., SYMB
  SYMB-MAP-ITEMS  ::= SYMB-OR-MAP
                    | SOME-SYMB-KIND SYMB-OR-MAP ,..., SYMB-OR-MAP
  SOME-SYMB-KIND  ::= sort/sorts | op/ops | pred/preds

! SYMB            ::= ID | ID : TYPE
! TYPE            ::= OP-TYPE | PRED-TYPE  
  SYMB-MAP        ::= SYMB "|->" SYMB                             
  SYMB-OR-MAP     ::= SYMB | SYMB-MAP

  SPEC-NAME       ::= SIMPLE-ID
  VIEW-NAME       ::= SIMPLE-ID
  TOKEN-ID        ::= ... | TOKEN [ ID ,..., ID ]
  MIXFIX-ID       ::= ... | TOKEN-PLACES [ ID ,..., ID ]

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk

Prev Up Next