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.