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.

See [AHMS99]

 

At the level of structured specifications we have the following encodings :

Back to roadmap