S-1 -- Structured Specifications

Go backward to Basic Specifications with Subsorts
Go up to Appendix A: Abstract Syntax
Go forward to Generic Specifications

Structured Specifications

SPEC            ::=   BASIC-SPEC | TRANSLATION | REDUCTION
                |     UNION | EXTENSION | FREE-SPEC | TYPE-DEFN-GROUP
TRANSLATION     ::=   translation SPEC SIG-MORPH
REDUCTION       ::=   reduction RESTRICTION SPEC 
RESTRICTION     ::=   restriction EXPOSURE SYMB+
EXPOSURE        ::=   hiding | revealing
SYMB            ::=   SORT | FUN-SYMB | PRED-SYMB
UNION           ::=   union SPEC+
EXTENSION       ::=   extension OF-SPEC* SPEC
OF-SPEC         ::=   PERSISTENT-SPEC | SPEC
PERSISTENT-SPEC ::=   persistent-spec SPEC
FREE-SPEC       ::=   free-spec SPEC

SIG-MORPH       ::=   sig-morph SYMB-MAP*
SYMB-MAP        ::=   SORT-MAP | FUN-SYMB-MAP | PRED-SYMB-MAP
SORT-MAP        ::=   sort-map SORT SORT
FUN-SYMB-MAP    ::=   fun-symb-map FUN-SYMB FUN-SYMB
PRED-SYMB-MAP   ::=   pred-symb-map PRED-SYMB PRED-SYMB

BASIC-ITEM      ::=   ... | TYPE-DEFN-GROUP
TYPE-DEFN-GROUP ::=   type-defn-group TYPE-DEFN+ AXIOM*
TYPE-DEFN       ::=   type-defn SORT ALTERNATIVE+
ALTERNATIVE     ::=   CONSTRUCT | SORT
CONSTRUCT       ::=   construct FUN-NAME COMPONENTS*
COMPONENTS      ::=   components FUN-NAME* SORT

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk