Automating Refinement of Circus Programs - Formal Methods: Foundations and Applications - page 288

6 Conclusions

We have presented a treatment of well-formedness in a shallow embedding of
Circus that considerably simplifies the provisos generated in the application of

refinement (and other) laws. Although it was described in the context of our
Circus mechanisation, the techniques and results obtained generalise to other

language embeddings in other tools that raise similar issues.
We have introduced the wd function to capture well-formedness of terms as
if they were syntactic rather than semantic entities. We have then identified
constraints to establish that this axiomatisation, though non-conservative, is
sound. We have thus avoided the added complexity of a deep embedding while
reaping some of its benefits in relation to properties that are inherently syntactic.
The underlying model for wd is actually a strict treatment of undefined values.
We, however, do not make its model explicit and content ourselves with its
mere existence. Since the logic of HOL does not accommodate undefinedness,
limitations arise in that we cannot, for instance, utilise wd on boolean functions
because the type

is not 'big enough' to provide enough values to represent the
undefined case. This is a trade off that we have to accept.
The wd function crucially paves the way for the ecient application of more
complex refinement tactics as it enabled us to recast the implementation of
ArcAngel C

B

in such a way that, apart from genuine proof obligations, only one
additional proviso is generated — to establish the well-definedness of the initial
program. This keeps the complexity of emerging refinement theorems at bay,
and thereby creates opportunities for the use of our mechanisation of Circus and

tools for automatic refinement in the context of real industrial systems.
In [17], von Wright presents a tool for stepwise refinement in a simple sequen-
tial command language. Its semantics is characterised in terms of wp predicate
transformers, which are shallowly embedded into HOL. Well-definedness condi-
tions loosely correspond to establishing the monotonicity of predicate transform-
ers, however the semantic domain is not apriori restricted to those.
The implication of von Wright's and similar approaches are that we required
more relaxed definitions of operators, and also accept limitations on what laws
can be generally established for the semantic entities. In the UTP, we often rely
on proving properties from healthiness conditions rather than by induction over
some syntax, which makes our approach more suitable here.
Other related work is the refinement editor Refine and Gabriel [14] which sup-
ports the specification and interactive application of ArcAngel tactics to derive
programs in Morgan's calculus. These tools notably offer facilities to interac-
tively apply tactics and laws. Otherwise, Refine and Gabriel were developed in
view of a specific language, and are essentially rewrite systems.
More recent work has been done on developing Saoith ın [1], a proof assistant
specifically designed for the UTP. Its advantages are that it essentially operates
at the level of syntax, and naturally some of the semantic issues we reported on
do not arise. It also provides proof strategies that are optimised for proofs in