We have shown that it is possible to write tools for a complex language with strong semantical bias (though it turns out to be a complex task). We could reduce the amount of work by re-using existing tools as much as possible. Moreover, by using a common tool interchange format, we have created a tool which can be used in connection with other tools as a front end or back end. Currently, our tool has been used in connection with two theorem provers (PVS and Isabelle) and one rewriting engine (ELAN). We have discussed some practical problems that arise when using an encoding into existing tools, rather than creating a new tool.
Finally, a generic static analysis of CASL structured specifications allows to re-use the tool also for other logics than the logic underlying CASL (for example, higher-order CASL, reactive CASL, temporal logic, or just your own favourite logic).
In the future, we hope that more tools will be integrated to work with our tools. An even better integration can be achieved with the UniForM workbench [KPO+99], which also provides library management and access to a generic transformation application system [LW99, LTKKB99] that will be instantiated to CASL.
Future work will turn our tool into a theorem proving environment that can be used for practical problems. On the way to this goal, we have to implement proof management, dealing with proof obligations, intended consequences and refinement. Moreover, special simplifiers and proof tactics for CASL will have to be developed an tested. A first case study will be the verification of proof obligations and intended consequences for the libraries of CASL basic datatypes [RM99].
A further topic that would be interesting is the study of the semantic relationships between the encoding of CASL into HOL and a true combination of CASL and HOL (like higher-order CASL [HKBM98]).
Another direction of research will further exploit the possibility of the generic analysis of CASL-in-the-large. It is possible to extend CASL to a heterogeneous specification language, where one can combine specifications written in several different logics, see [Tar99] for some first ideas. Tool support for such a language would extend the generic analysis of CASL-in-the-large with an analysis of structuring mechanisms for moving specifications between different logics.