Information Technology Reference
In-Depth Information
lemma
ref pp assign :
pp (true) (
λ
g.
λ
g1.((getNatOfPath g1 p) = n)) [p] ref
(assign p (Val (Zint n)))
The proof of this lemma, together with the proofs of other useful lemmas, can
be found at
http://isg.rhul.ac.uk/morisset/sbmf/rcos lib.thy
.
Another example is the Expert Pattern, which is an essential rule for
oo
functionality decomposition by delegating responsibilities through method calls
to the objects, called the experts, that have the information to carry out the
responsibilities. For instance, defining a setter for a field is a special case of the
Expert Pattern, and therefore a refinement. In this case, we have proved, with
the theorem
EPIsRefOne
, that the method
bar()
{
p.x := n
}
is refined by the
method
bar()
{
p.m()
}
where
m()
{
this
.x := n
}
is a method of
p
, for any non-
empty path
p
and constant
n
; a similar theorem
EPIsRefTwo
is provided, when the
setter takes the value as an argument, that is, the method
bar()
{
p.x := n
}
is
refined by the method
bar()
{
p.m(n)
}
where
m(Tv)
{
this
.x := v
}
is a method
of
p
, for any primitive type
T
and parameter
v
.
6.3 Example
Let us consider the examples given in Section 2. The user first defines the classes
A
and
B
1
and then introduces a manual refinement, concerning the operation
foo
, where the old design is
d
old
=
[
true
|−
a.x'=2
∨
a.x'=3]
and the new design is
d
new
=
{
a.m(1) ; a.x := a.x + 1
}
. When applying the refinement, the class
B
3
is
obtained. However, proving directly that
d
old
is refined by
d
new
might be com-
plex, as several steps of refinement are involved. The user can either decompose
the refinement proof in Isabelle or directly in the rCOS tool. Indeed, the latter
allows one to easily compose refinement steps. In this example, the user can intro-
duce the manual refinement
r
1
of
[
true
|−
a.x'=2
∨
a.x'=3]
to
[
true
|−
a.x'=2]
;the
automatic refinement
r
2
of pre/post-conditions to assignments; the the manual
refinement
r
3
of
a.x := 2
to
a.x:=1; a.x := a.x+1
; the expert-pattern refinement
r
4
on
a.x := 1
.
The proof obligations for each step can be generated automatically. For in-
stance, the proof obligation corresponding to
r
3
is the following statement:
assign this .a.x (Val (Zint 2)) ref
(assign this .a.x (Val (Zint 1))
;
(assign this .a.x (Plus (Path this.a.x) (Val (Zint 1)))))
The refinement
r
1
strengthens the post-condition of the design, so the proof
is quite straight-forward. The proofs of
r
2
,r
3
and
r
4
directly follow from the
lemmas described in the previous subsection. Finally, using the fact that the re-
finement relation is transitive, we can prove that
d
old
=
[
true
|−
a.x'=2
∨
a.x'=3]
is refined by
d
new
=
{
a.m(1) ; a.x := a.x + 1
}
. The complete proofs can be found
at
http://isg.rhul.ac.uk/morisset/sbmf/example.thy
. Except the proofs of
r
1
and
r
3
, all the other proofs could be derived automatically, since automatic
Search WWH ::
Custom Search