CRefine is a tool that can be used throughout the refinement of concurrent systems in a calculational approach. It automates the application of the Circus refinement calculus by applying various well-proved refinement laws, sometimes with the discharge of proof obligations, most of which are automatically proved. CRefine also automates the process of defining and applying refinement tactics in a program development as a single transformation rule. The tactics are formalized in ArcAngelC, a refinement tactic language for Circus programs. Finally, CRefine can also generate Java object-code (using JCircus, a code generator from Circus to Java) that implements the behaviour of the input specification in Circus.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
