Up Next
Go up to B Abbreviated Abstract Syntax
Go forward to B.2 Structured Specifications

B.1 Basic and Subsorted Specifications

  BASIC-SPEC       ::= basic-spec BASIC-ITEMS*

  BASIC-ITEMS      ::= SIG-ITEMS 
                     | free-datatype DATATYPE-DECL+
                     | sort-gen SIG-ITEMS+
                     | var-items VAR-DECL+ 
                     | local-var-axioms VAR-DECL+ FORMULA+
                     | axiom-items FORMULA+

  SIG-ITEMS        ::= sort-items SORT-ITEM+
                     | op-items OP-ITEM+
                     | pred-items PRED-ITEM+
                     | datatype-items DATATYPE-DECL+

  SORT-ITEM        ::= sort-decl SORT+
                     | subsort-decl SORT+ SORT
                     | subsort-defn SORT VAR SORT FORMULA
                     | iso-decl SORT+

  OP-ITEM          ::= op-decl OP-NAME+ OP-TYPE OP-ATTR*
                     | op-defn OP-NAME  OP-HEAD TERM
  OP-TYPE          ::= total-op-type   SORTS SORT
                     | partial-op-type SORTS SORT
  SORTS            ::= sorts SORT*
  OP-ATTR          ::= associative | commutative | idempotent
                     | unit-op-attr TERM
  OP-HEAD          ::= total-op-head   ARG-DECL* SORT
                     | partial-op-head ARG-DECL* SORT
  ARG-DECL         ::= arg-decl VAR+ SORT

  PRED-ITEM        ::= pred-decl PRED-NAME+ PRED-TYPE
                     | pred-defn PRED-NAME  PRED-HEAD FORMULA
  PRED-TYPE        ::= pred-type SORTS
  PRED-HEAD        ::= pred-head ARG-DECL*

  DATATYPE-DECL    ::= datatype-decl SORT ALTERNATIVE+
  ALTERNATIVE      ::= total-construct   OP-NAME COMPONENTS*
                     | partial-construct OP-NAME COMPONENTS*
                     | subsorts SORT+
  COMPONENTS       ::= total-select   OP-NAME+ SORT
                     | partial-select OP-NAME+ SORT
                     | SORT

  VAR-DECL         ::= var-decl VAR+ SORT

  FORMULA          ::= quantification QUANTIFIER VAR-DECL+ FORMULA
                     | conjunction FORMULA+
                     | disjunction FORMULA+
                     | implication FORMULA FORMULA
                     | equivalence FORMULA FORMULA
                     | negation FORMULA
                     | true | false
                     | predication PRED-SYMB TERMS
                     | definedness TERM
                     | existl-equation TERM TERM
                     | strong-equation TERM TERM
                     | membership TERM SORT
  QUANTIFIER       ::= forall | exists | exists-uniquely
  PRED-SYMB        ::= PRED-NAME | QUAL-PRED-NAME
  QUAL-PRED-NAME   ::= qual-pred-name PRED-NAME PRED-TYPE

  TERMS            ::= terms TERM*
  TERM             ::= SIMPLE-ID
                     | qual-var VAR SORT
                     | application OP-SYMB TERMS
                     | sorted-term TERM SORT
                     | cast TERM SORT
                     | conditional TERM FORMULA TERM
  OP-SYMB          ::= OP-NAME | QUAL-OP-NAME
  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-places 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