In this work, we present a formal definition of Circus type system, with the intention of assisting the development of a type checker for this language. At first, we define the Circus type rules, and afterwards we describe how we implemented the type checker using a direct mapping of the type rules to code. This contributed for the robust construction of the type checker. The developed type checker also offers extra facilities, such as the annotation of type information for each fragment of a specification or program, and the availability of clear and objective error messages. Additionally, we projected the type checker as a component of easy integration, maintenance and extension.
With the definition of the Circus type system and the implementation of its type checker, we believe that we are giving an important contribution in the evolution of Circus, clarifying essential points of its definition as a strongly typed language that is compatible with Z and CSP. Additionally, we are also contributing for the development of other tools for Circus. We hope that our work can serve as base for the definition and implementation of the type systems of the Circus extensions.
This tool is a syntax type checker for Circus specifications, which is implemented in Java.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
