Information Technology Reference
In-Depth Information
A general issue with the mechanisation is the large number of provisos raised
by the application of refinement laws. They are mostly conditions that we would
not deal with in a pen-and-paper proof. For example, the associativity law
a
1
;
;
;
;
≡
a
3
for actions does not require any provisos to
be discharged when applied in a pen-and-paper proof. This is not so in its en-
coding in the semantic embedding of
(
a
2
a
3
)
(
a
1
a
2
)
Circus
,whichisgivenbelow.
∀
a
1
,
a
2
,
a
3
:
CIRCUS ACTION
|
;
C
(
a
2
;
C
a
3
)
≡
(
a
1
;
C
a
2
)
;
C
a
3
α
a
1
=
α
a
2
∧
α
a
2
=
α
a
3
•
a
1
First, we have to introduce the provisos that
a
1
,
a
2
and
a
3
belong to the set
CIRCUS ACTION
, the semantic domain for actions. Secondly, two provisos
are needed to ensure that all actions have the same alphabet. The
α
operator
gives the alphabet of an action: the variables on which it operates.
These provisos establish well-formedness constraints that are typically taken
for granted given the syntactic and type correctness of the actions. A mechanised
model, however, forces us to make them explicit to establish the necessary assump-
tions for provability of the laws. Each
operator, like sequential composition
of actions above, is encoded by a semantic function [12], and these functions are
total on
CIRCUS ACTION
, but only partial with respect to the corresponding
maximal set. This gives rise to non-trivial constraints, since
CIRCUS ACTION
,
in our model, is not a type in the sense of being maximal.
In a deep semantic embedding, it is possible to formalise well-formedness
as a property of the program syntax. (The difference between a shallow and
deep embedding is that the latter also formalises the syntax of the embedded
language.) We can then prove that (syntactic) well-formedness implies mem-
bership to the aforementioned (semantic) domains. Additionally, a collection
of laws may be used to deduce well-formedness of compound expressions from
the well-formedness of its components, or conversely, deduce well-formedness of
components from the well-formedness of the expression as a whole.
There are, however, important reasons for not pursuing a deep approach in
our mechanisation of the UTP and
Circus
Circus
to encode alphabetised predicates. The
most crucial one is that the language of the UTP is not static: in higher-level
theories new operators may be introduced that effectively become part of the
syntax. In a deep embedding such extensions would be dicult to handle.
In combination with our implementation of
ArcAngel
C
and more complex re-
finement tactics, the problem of provisos is exacerbated by the fact that tactic
application relies on so-called 'model theorems', monotonicity of operators, and
reflexivity and transitivity of refinement. Those theorems are frequently applied
as part of many of the core tactics and suffer from the same problem of in-
troducing conceptually superfluous provisos. Executing the tactics, the provisos
quickly accumulate and result in theorems that become unmanageable.
Our contribution is a novel treatment of the notion of well-formedness at
the semantic level. It allows us to eliminate most of the inherent provisos in law
applications with minimal incisions to the embedding. To take advantage of that,
we have made changes to the implementation of
ArcAngel
C
as given in [18]; we
Search WWH ::
Custom Search