FCasEnv
FCasEnv is a format for the CASL global environment,
based on the CasEnv format.
It contains, for each specification, a signature
plus a set of axioms. Thus, the structure of the
specification is not available.
This is useful in connection with theorem provers
or rewriting engines that can handle only
flat specifications.
Within the CASl tool set, you can use the
option -env=FCasEnv to generate the FCasEnv format.
The following grammar describes the FCasEnv format:
FCASENV ::= fcasenv ( f-global-entry-tuple* ( F-GLOBAL-ENTRY-TUPLE* )
F-GLOBAL-ENTRY-TUPLE ::= f-global-entry-tuple ( SIMPLE-ID, F-GLOBAL-ENTRY )
F-GLOBAL-ENTRY ::= f-spec-defn-env ( F-GENERICITY-ENV, EXT-SIGNATURE )
| f-view-defn-env ( F-GENERICITY-ENV, EXT-SIGNATURE,
MORPHISM, EXT-SIGNATURE )
| f-arch-spec-defn-env
| f-unit-spec-defn-env
F-GENERICITY-ENV ::= f-genericity-env ( EXT-SIGNATURE, ext-signature*
( EXT-SIGNATURE* ) )
EXT-SIGNATURE ::= ext-signature ( SIGNATURE, SIGNATURE,
formula* ( FORMULA* ) )
Further rules are contained in the common part
of CasEnv and FCasEnv.