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

Basic Specifications

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

  SIG-DECL         ::=  SORT-DECL | FUN-DECL | PRED-DECL
  SORT-DECL        ::=  sort-decl SORT+
  FUN-DECL         ::=  fun-decl FUN-NAME+ FUN-TYPE
  PRED-DECL        ::=  pred-decl PRED-NAME+ PRED-TYPE
! FUN-TYPE         ::=  SORT | PARTIAL-CON-TYPE | 
!                    |  TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
! PARTIAL-CON-TYPE ::=  partial-con-type SORT
! TOTAL-FUN-TYPE   ::=  total-fun-type SORT+ SORT
! PARTIAL-FUN-TYPE ::=  partial-fun-type SORT+ SORT
  PRED-TYPE        ::=  pred-type 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 TERM*
  DEFINEDNESS      ::=  definedness TERM
! EXISTL-EQUATION  ::=  existl-equation TERM TERM
! STRONG-EQUATION  ::=  strong-equation TERM TERM

! TERM             ::=  VAR | CONSTANT | APPLICATION | SORTED-TERM
! CONSTANT         ::=  FUN-SYMB
! APPLICATION      ::=  application FUN-SYMB TERM+
  SORTED-TERM      ::=  sorted-term TERM SORT

  SORT-GEN         ::=  sort-gen SORT+ FUN-SYMB+

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

! ATTRIBUTION      ::=  attribution PROPERTY+ FUN-SYMB+
! PROPERTY         ::=  SIMPLE-PROPERTY | UNIT-PROPERTY
! SIMPLE-PROPERTY  ::=  associative | commutative | idempotent
! UNIT-PROPERTY    ::=  unit-property FUN-SYMB

  FUN-SYMB         ::=  fun-symb FUN-NAME FUN-TYPE?
  PRED-SYMB        ::=  pred-symb PRED-NAME PRED-TYPE?

  SORT             ::=  ID
  FUN-NAME         ::=  ID
  PRED-NAME        ::=  ID
  VAR              ::=  SIMPLE-ID
CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk