| The CASL tool set | |
 |
Features |
|
Architecture |
 |
Parsers |
|
Static Analysis |
|
Formatter |
|
|
Flat Encodings |
|
|
Structured Encodings |
| |
Construct development graph |
The static analysis is available within the CASL tool set (CATS).
Static analysis does the following :
- for each specification, construction of the current signature (local environment) ;
- using the local environment, mixfix analysis of terms and formulas ;
- overload resolution of terms and formulas ;
- construction of a global environment.Within the CASL tool set, you can use the option -input=static to switch on the static analysis.
The LL(2)-parser and the HOL-CASL parsers are available within the CASL tool set (CATS).
CasEnv is a format for the CASL global environment, based on ATerms.
A detailed description can be found here.
A library of CASL specifications in ASCII format, following the syntax of CASL as described in Appendix C of the CASL Summary.
[click !]
[click !]
[click !]
The LaTeX formatter is available within the CASL tools set (CATS).
It converts the specification(s) to LaTeX code depending on the file casl.sty, version 1.3.
It does not yet format architectural specifications and semantic annotations.
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.HCasEnv contains, for each specification, additionally a signature fragment corresponding to those parts of the specification that have been hidden.
A more detailed description will follow.
 |
||||
 |
||||
 |
||||
 |
||||
 |
||||
|
|
||||
 |
||||
|
|
||||
 |
 |
 |
 |
|
|
|
|
|||
 |
||||
|
|
||||
|
||||
|
|
||||
 |
||||
|
|
 |
|||
 |
|
|||
|
|
 |
|||
 |
||||
|
|
|
|||
 |
|
|||
|
|
OMDOC
|
|||
The interchange formats CasFix, CasEnv, HCasEnv and FCasEnv are all based on the ATerm interchange format.
The provers and rewriters
are not part of the CASL tool set, but rather are separately available
tools. They are listed here for the sake of completeness.
