Up to now only tools for the development of specifications have been implemented in the Spectrum project.
The RAP&TIP system is an environment for prototyping hierarchical algebraic specifications; moreover it includes an inductive theorem prover for equational formulas [Frau 91].
The ISAR system gives support for the correctness proof of
behavioural implementations
[4][Baue 91].
The main technique is
context induction which is performed with the help of TIP.
Components of RAP specifications can be designed interactively with the help of the Specifiers Notepad [Breu 90].