Up Next
Go up to A Abstract Syntax
Go forward to A.2 Basic Specifications with Subsorts

A.1 Basic Specifications

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

  BASIC-ITEMS      ::= SIG-ITEMS | FREE-DATATYPE | SORT-GEN
                     | VAR-ITEMS | LOCAL-VAR-AXIOMS | AXIOM-ITEMS

  SIG-ITEMS        ::= SORT-ITEMS | OP-ITEMS | PRED-ITEMS
                     | DATATYPE-ITEMS

  SORT-ITEMS       ::= sort-items SORT-ITEM+
  SORT-ITEM        ::= SORT-DECL

  SORT-DECL        ::= sort-decl SORT+

  OP-ITEMS         ::= op-items OP-ITEM+
  OP-ITEM          ::= OP-DECL | OP-DEFN

  OP-DECL          ::= op-decl OP-NAME+ OP-TYPE OP-ATTR*
  OP-TYPE          ::= TOTAL-OP-TYPE | PARTIAL-OP-TYPE
  TOTAL-OP-TYPE    ::= total-op-type SORTS SORT
  PARTIAL-OP-TYPE  ::= partial-op-type SORTS SORT
  SORTS            ::= sorts SORT*
  OP-ATTR          ::= BINARY-OP-ATTR | UNIT-OP-ATTR
  BINARY-OP-ATTR   ::= associative | commutative | idempotent
  UNIT-OP-ATTR     ::= unit-op-attr TERM

  OP-DEFN          ::= op-defn OP-NAME OP-HEAD TERM
  OP-HEAD          ::= TOTAL-OP-HEAD | PARTIAL-OP-HEAD
  TOTAL-OP-HEAD    ::= total-op-head ARG-DECL* SORT
  PARTIAL-OP-HEAD  ::= partial-op-head ARG-DECL* SORT
  ARG-DECL         ::= arg-decl VAR+ SORT

  PRED-ITEMS       ::= pred-items PRED-ITEM+
  PRED-ITEM        ::= PRED-DECL | PRED-DEFN

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

  DATATYPE-ITEMS   ::= datatype-items DATATYPE-DECL+
  DATATYPE-DECL    ::= datatype-decl SORT ALTERNATIVE+
  ALTERNATIVE      ::= TOTAL-CONSTRUCT | PARTIAL-CONSTRUCT
  TOTAL-CONSTRUCT  ::= total-construct   OP-NAME COMPONENTS*
  PARTIAL-CONSTRUCT::= partial-construct OP-NAME COMPONENTS*
  COMPONENTS       ::= TOTAL-SELECT | PARTIAL-SELECT | SORT
  TOTAL-SELECT     ::= total-select   OP-NAME+ SORT
  PARTIAL-SELECT   ::= partial-select OP-NAME+ SORT

  FREE-DATATYPE    ::= free-datatype DATATYPE-ITEMS

  SORT-GEN         ::= sort-gen SIG-ITEMS+

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

  LOCAL-VAR-AXIOMS ::= local-var-axioms VAR-DECL+ AXIOM+

  AXIOM-ITEMS      ::= axiom-items AXIOM+     

  AXIOM            ::= FORMULA
  FORMULA          ::= QUANTIFICATION | CONJUNCTION | DISJUNCTION 
                     | IMPLICATION | EQUIVALENCE | NEGATION | ATOM
  QUANTIFICATION   ::= quantification QUANTIFIER VAR-DECL+ FORMULA
  QUANTIFIER       ::= forall | exists | exists-uniquely
  CONJUNCTION      ::= conjunction FORMULA+
  DISJUNCTION      ::= disjunction FORMULA+
  IMPLICATION      ::= implication FORMULA FORMULA
  EQUIVALENCE      ::= equivalence FORMULA FORMULA
  NEGATION         ::= negation FORMULA

  ATOM             ::= TRUTH | PREDICATION | DEFINEDNESS 
                     | EXISTL-EQUATION | STRONG-EQUATION
  TRUTH            ::= true | false
  PREDICATION      ::= predication PRED-SYMB TERMS
  PRED-SYMB        ::= PRED-NAME | QUAL-PRED-NAME
  QUAL-PRED-NAME   ::= qual-pred-name PRED-NAME PRED-TYPE
  DEFINEDNESS      ::= definedness TERM
  EXISTL-EQUATION  ::= existl-equation TERM TERM
  STRONG-EQUATION  ::= strong-equation TERM TERM

  TERMS            ::= terms TERM*
  TERM             ::= SIMPLE-ID | QUAL-VAR | APPLICATION
                     | SORTED-TERM | CONDITIONAL
  QUAL-VAR         ::= qual-var VAR SORT
  APPLICATION      ::= application OP-SYMB TERMS
  OP-SYMB          ::= OP-NAME | QUAL-OP-NAME
  QUAL-OP-NAME     ::= qual-op-name OP-NAME OP-TYPE
  SORTED-TERM      ::= sorted-term TERM SORT
  CONDITIONAL      ::= conditional TERM FORMULA TERM

  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-PLACES     ::= 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