Up Next
Go up to C.2 Context-Free Syntax
Go forward to C.2.2 Structured Specifications

C.2.1 Basic Specifications with Subsorts

  BASIC-SPEC      ::= BASIC-ITEMS...BASIC-ITEMS  |  { }

  BASIC-ITEMS     ::= SIG-ITEMS 
                    | free      type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
                    | generated type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/
                    | generated { SIG-ITEMS...SIG-ITEMS } ;/
                    | var/vars VAR-DECL ;...; VAR-DECL ;/
                    | var/vars VAR-DECL ;...; VAR-DECL
                               "." FORMULA "."..."." FORMULA ;/
                    | axiom/axioms FORMULA ;...; FORMULA ;/

  SIG-ITEMS       ::= sort/sorts SORT-ITEM ;...; SORT-ITEM ;/
                    | op/ops OP-ITEM ;...; OP-ITEM ;/
                    | pred/preds PRED-ITEM ;...; PRED-ITEM  ;/
                    | type/types DATATYPE-DECL ;...; DATATYPE-DECL ;/

  SORT-ITEM       ::= SORT ,..., SORT 
                    | SORT ,..., SORT < SORT 
                    | SORT = { VAR : SORT "." FORMULA } 
                    | SORT =...= SORT                       

  OP-ITEM         ::= OP-NAME ,..., OP-NAME : OP-TYPE
                    | OP-NAME ,..., OP-NAME : OP-TYPE , OP-ATTR ,..., OP-ATTR 
                    | OP-NAME OP-HEAD = TERM

  OP-TYPE         ::= SOME-SORTS  -> SORT  |  SORT                      
                    | SOME-SORTS  ->? SORT  |  ? SORT                    

  SOME-SORTS      ::= SORT *...* SORT 

  OP-ATTR         ::= assoc  |  comm  |  idem  |  unit TERM

  OP-HEAD         ::= ( ARG-DECL ;...; ARG-DECL ) : SORT   |  :  SORT   
                    | ( ARG-DECL ;...; ARG-DECL ) :? SORT  |  :? SORT 
  ARG-DECL        ::= VAR ,..., VAR : SORT

  PRED-ITEM       ::= PRED-NAME ,..., PRED-NAME : PRED-TYPE 
                    | PRED-NAME PRED-HEAD <=> FORMULA
                    | PRED-NAME <=> FORMULA 

  PRED-TYPE       ::= SOME-SORTS  |  ( )

  PRED-HEAD       ::= ( ARG-DECL ;...; ARG-DECL )

  DATATYPE-DECL   ::= SORT "::=" ALTERNATIVE "|"..."|" ALTERNATIVE
  ALTERNATIVE     ::= OP-NAME  ( COMPONENT ;...; COMPONENT )    
                    | OP-NAME  ( COMPONENT ;...; COMPONENT )?   
                    | OP-NAME                           
                    | sort/sorts SORT ,..., SORT 
  COMPONENT       ::= OP-NAME ,..., OP-NAME :  SORT
                    | OP-NAME ,..., OP-NAME :? SORT               
                    | SORT                                        

  VAR-DECL        ::= VAR ,..., VAR : SORT

  FORMULA         ::= QUANTIFIER  VAR-DECL ;...; VAR-DECL "." FORMULA
                    | FORMULA /\ FORMULA /\.../\ FORMULA
                    | FORMULA \/ FORMULA \/...\/ FORMULA
                    | FORMULA => FORMULA
                    | FORMULA if FORMULA
                    | FORMULA <=> FORMULA
                    | not FORMULA
                    | true | false
                    | PRED-SYMB
                    | PRED-SYMB ( TERMS )
                    | TERM TERM...TERM
                    | def TERM
                    | TERM =e= TERM
                    | TERM = TERM
                    | TERM in SORT
                    | ( FORMULA )

  QUANTIFIER      ::= forall  |  exists  |  exists!

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

  TERMS           ::= TERM ,..., TERM

  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 QUAL-OP-NAME )
  QUAL-OP-NAME    ::= OP-NAME : OP-TYPE

  SORT            ::= TOKEN-ID
  OP-NAME         ::= ID
  PRED-NAME       ::= ID
  VAR             ::= SIMPLE-ID 

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

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

Up Next