![Next](http://www.daimi.aau.dk/images/next.xbm)
Go backward to 3 Different formats needed for tools
Go up to Top
Go forward to 5 Documentation tools and educational tools
4 Prototyping and verification tools
Different kinds of tools are planned.
- Prototyping tools:
A rewrite engine for the largest possible subset of CASL should be provided.
- A generator of proof obligations related to the construction
of modules or to the refinement process should be provided.
- First-order theorem provers.
The proof obligations should be sent to general provers.
Two options are possible and maybe complementary:
- Design or reuse of specific tools for several subsets of CASL:
equational, conditional, full first-order logic with
total functions, total functions with subsorts, partial functions,...
Once the interoperability format is fixed,
it should be precisely experimented how to proceed to reuse an
existing tool.
- Encode CASL (or more precisely its underlying logic)
into total first-order logic and first-order theorem
provers.
Such an encoding has been already done in HOL.
CoFI
Document: CASL/Tools ---- 20 May 1997.
Comments to cofi-tools@brics.dk
![Next](http://www.daimi.aau.dk/images/next.xbm)