Information Technology Reference
In-Depth Information
g
k
−
1
×
p
o
g
1
g
i
−
1
f
=
g
i
=
g
k
g
i
+
1
q
g
k
+
1
g
n
Fig. 3.
Example with two indexes
i
<
k
in
K
pos
4.3 PVS Formalisation
Given a list of names
fs
, the dot composition of the corresponding attributes is
formalised as
=
multidot
(
fs : list
[
Name
])
:
RECURSIVE
Expr
IF
null?
(
fs
)
THEN
Current
ELSIF
null?
(
cdr
(
fs
))
THEN
car
(
fs
)
ELSE
car
(
fs
)
multidot
(
cdr
(
fs
))
MEASURE
length
(
fs
)
Note that because
e
Current
=
e
does not hold when
e
evaluates to void, we
cannot simply append
Current
at the end of the multidot expression.
As an example of the PVS formalisation, we show a property that combines
empty
_
K
pos
and
max
_
K
pos
in a property at the source code level. Since it is
written as an equality between functions, it can be used as a rewrite rule.
multidot_after_assignment_pos :
LEMMA
∀
(
f : Name
,
gs : list
[
Name
],
x
,
e : Expr
,
o:Object
v
⊥
,
h:Heap
⊥
)
:
((
x
f:
=
e
;
multidot
(
gs
))(
o
,
h
)
=
LET
h
=
(
x
f:
=
e
)(
o
,
h
),
K
pos
=
λ
(
k: below
[
length
(
hs
)])
:
x
(
o
,
h
)
multidot
(
take
(
gs
,
k
))(
o
,
h
)
=
∧
=
nth
(
gs
,
k
)
f
IN
IF
bottom?
(
h
)
THEN
bottom
ELSIF
empty?
(
K
pos
)
THEN
multidot
(
gs
)(
o
,
h
)
ELSE LET
k
=
max
(
K
pos
)
IN
=
length
(
gs
)
-
1
THEN
e
(
o
,
h
)
ELSE
(
e
multidot
(
drop
(
gs
,
k+1
)))(
o
,
h
)
This property describes in terms of
h
all the possible outcomes of
multidot
(
gs
)
when evaluated in
h
. If the assignment resulted in an error then the result is an
IF
k
Search WWH ::
Custom Search