Information Technology Reference
In-Depth Information
involving expressions are parameterised in terms of
WT EXPRESSION
,their
domains are not maximal, and so we can give
wd
axioms for them.
We do not actually define our model for
wd
in
ProofPower-Z
,asitwould
unnecessarily complicate the various definitions of operators. The main point
is that we can introduce
wd
capturing the well-formedness of terms purely in
semantic terms, and given the above caveats this definition is sound.
It is now possible to specify laws that either exploit or prove
wd
theorems. In
particular, the associativity law for conjunction is now expressible as below.
∀
p
1
,
p
2
,
p
3
:
U
|
wd
((
p
1
∧
P
p
2
)
∧
P
p
3
)
•
(
p
1
∧
P
p
2
)
∧
P
p
3
≡
p
1
∧
P
(
p
2
∧
P
p
3
)
∧
wd
(
p
1
∧
P
(
p
2
∧
P
p
3
))
This directly mirrors the intuition that if the left-hand side
p
1
∧
P
(
p
2
∧
P
p
3
)is
well-defined, the equivalence holds and also the right-hand side (
p
1
∧
P
p
3
is well-defined. Its only non-trivial proviso is the assumption of well-definedness
of the initial program. We mechanically proved the above law without much
effort by utilising its original version and rewriting applications of
wd
.
This illustrates how
wd
can provide a framework in which we can handle the
emerging proof obligations for typing with theorems that establish that well-
formedness is preserved. We work in a setting similar to that of pen-and-paper
refinement proofs, where we normally assume that the initial program is well-
formed, as are the programs of each law. If additionally the arguments of param-
eterised laws are well-formed, we conclude that all programs in the derivation
chain must be well-formed. In summary, we work under assumptions that mean
that we do not need to worry about issues of well-formedness.
In the following section we explain how the implementation of
ArcAngel
C
p
2
)
∧
P
has
been amended to make use of theorems that possess this shape.
4Ex en onstothe
ArcAngelC
Implementation
We present here how we have extended the
ArcAngel
implementation to take
advantage of the
wd
function.
4.1 Extended Refinement Theorems
Refinement theorems in our implementation of
ArcAngel
C
had to be of the form
Γ
B
, where Γ is a list of proof obligations, and
A
and
B
are program
expressions. To integrate well-definedness constraints, we have generalised the
permissible shape of such theorems to Γ
,
wd A
A
wd B
.Wecallthem
extended refinement theorems
. Their conclusions are conjunctions in which the
first conjunct provides the actual refinement, and the second conjunct establishes
well-definedness of the result
B
of the program transformation. We also have an
assumption that asserts well-definedness of the initial program
A
.
The implementation has been adapted to handle these kinds of theorems.
Importantly, the
ArcAngel
C
A
B
∧
mechanics has been adjusted as to only retain the
wd
theorem of the initial program, and, as much as possible, discard intermediate
wd
Search WWH ::
Custom Search