CasEnv is a format for the CASL global environment, based
on ATerms.
A more detailed description will follow.
The idea is to push the hiding to the outermost level, by
renaming any symbols that are hidden at different places to avoir name
clashes.
HCasEnv contains, for each specification, additionally a signature
fragment corresponding to those parts of the specification that have
been hidden.
Within the CASL tool set, you can use the option -env=HCasEnv to
generate the HCasEnv format.
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.
A more detailed description is available here.
This encoding flattens a structured specification into a signature
plus a set of axioms.
Within the CASL tool set, you can use the option -env=FCasEnv to
generate the FCasEnv format.
|
|
At the level of structured specifications we have the following encodings
:
Within the CASL tool set, you can use the option -env=HCasEnv or -env=FCasEnv
to generate the encodings.
|