Basic Specifications

BASIC-SPEC       ::=  basic-spec BASIC-ITEM*
BASIC-ITEM       ::=  SIG-DECL | VAR-DECL | AXIOM | SORT-GEN 
                   |  LOCAL-BASIC-SPEC

SIG-DECL         ::=  SORT-DECL | FUN-DECL | FUN-DEFN | PRED-DECL 
                   |  DATATYPE-DECL

SORT-DECL        ::=  sort-decl SORT+

FUN-DECL         ::=  fun-decl FUN-NAME+ FUN-TYPE FUN-ATTR*
FUN-TYPE         ::=  TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
TOTAL-FUN-TYPE   ::=  total-fun-type SORTS SORT
PARTIAL-FUN-TYPE ::=  partial-fun-type SORTS SORT
FUN-ATTR         ::=  BINARY-FUN-ATTR | UNIT-FUN-ATTR
BINARY-FUN-ATTR  ::=  associative | commutative | idempotent
UNIT-FUN-ATTR    ::=  unit-fun-attr FUN-SYMB
FUN-DEFN         ::=  fun-defn FUN-NAME VAR-DECL* SORT TERM

PRED-DECL        ::=  pred-decl PRED-NAME+ PRED-TYPE
PRED-TYPE        ::=  pred-type SORTS

SORTS            ::=  sorts SORT*

DATATYPE-DECL    ::=  datatype-decl SORT ALTERNATIVE+
ALTERNATIVE      ::=  CONSTRUCT 
CONSTRUCT        ::=  construct FUN-NAME COMPONENT*
COMPONENT        ::=  component FUN-NAME? SORT

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

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-symb PRED-NAME PRED-TYPE?
DEFINEDNESS      ::=  definedness TERM
EXISTL-EQUATION  ::=  existl-equation TERM TERM
STRONG-EQUATION  ::=  strong-equation TERM TERM

TERMS            ::=  terms TERM*
TERM             ::=  VAR | APPLICATION | SORTED-TERM
APPLICATION      ::=  application FUN-SYMB TERMS
FUN-SYMB         ::=  fun-symb FUN-NAME FUN-TYPE?
SORTED-TERM      ::=  sorted-term TERM SORT

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

LOCAL-BASIC-SPEC ::=  local-basic-spec BASIC-SPEC BASIC-SPEC

SORT             ::=  ID
FUN-NAME         ::=  ID
PRED-NAME        ::=  ID
VAR              ::=  SIMPLE-ID

---

CoFI Document: CASL/Summary-v0.97 --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk