A Concurrent Language for Refinement
Jim Woodcock, Ana Cavalcanti · Electronic workshops in computing · 2001
We present a combination of the well-established formal specification languages Z and CSP; our objective is to provide support for the specification of both data and behaviour aspects of concurrent systems, and a development technique. The resulting language, Circus , distinguishes itself in that it is aimed at the calculational refinement of specifications to programs written in a language similar to occam and Handel-C . In this paper, we present Circus , the rationale for its design, and a case study in its use.