Implementing Tactics of Refinement in CRefine

Circus

is a formal language that combines Z and CSP, providing support for specification of both data and behavioural aspects of concurrent systems. Furthermore,

Circus

has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise this application as a refinement tactic, which can then be used as a single transformation rule.

CRefine

was developed to automate the

Circus

refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. In this paper, we present an extension to

CRefine

: a new module that automates the process of defining and applying refinement tactics formalised in the tactic language

ArcAngel

C

. Finally, we illustrate the usefulness of the extension in the development of an industrial case study.