Information Technology Reference
In-Depth Information
where, for the sake of readability, we write a path as in code, e.g.
a.b.x
stands
for the path
[''x'',''b'',''a'']
.
Assignment.
The definition of the assignment is changed as follows.
definition
assign :: path
⇒
exp
⇒
(graph pred)
⇒
(graph pred)
where
assign p e q
≡ λ
u. wfGraph u & wfPath p u & wfExp e u &
q (swingPath p (getNodeExp e u) u)
where the path
p
is assigned to the expression
e
, which is required to be well-
formed. The function
getNodeExp
returns the value of an expression, which is
defined using
getVertexPath
when the expression to be evaluated is a path, oth-
erwise itself when it is a constant value.
Local Declaration and Un-declaration.
The commands
begin
and
end
de-
clare/initialize new local variables and terminate them, respectively.
definition
begin :: labelExpF
⇒
(graph pred)
⇒
(graph pred)
where
begin f q
≡ λ
u. wfGraph u & wflabelExpF f u & q (Vars f u)
definition
end :: (graph pred)
⇒
(graph pred)
where
end q
≡ λ
u. wfGraph u & q (removeSnode u)
where
f
is a well-formed function of type
labelExpF
, which means that for each
local variable, it is initialised by a well-formed expression in
f
.
The command
locdec
defines the block for local declaration and un-
declaration, where
f
is the same as above and
c
is the body of the block.
definition
locdec :: labelExpF
⇒
(graph predT)
⇒
(graph predT)
where
locdec f c
≡
begin f
;
c
;
end
Method Invocation.
The command
method
implements a method invocation
with the help of the command
locdec
.
definition
method :: (label
∗
exp) list
⇒
(graph predT)
⇒
(graph predT)
where
method l c
≡
locdec (getLabelExpF l) c
where
l
is of type
(label * exp) list
, each pair consisting of a formal value
parameter and the corresponding actual value parameter of the method, and
c
is
the method body followed by the assignment from the formal return parameter to
the actual return parameter. In the
method
command, the function
getLabelExpF
translates a list of pairs of type
label * exp
to the corresponding mapping of
type
labelExpF
(i.e.
label
⇒
exp
). For instance, the method call
a.m(1)
in the
example of Section 2 is translated as:
method [(
this
,Path
this.a
), (
v
, Val (Zint 1))]
;
assign
this.x
Path
v
When the method is called, the variable
this
is initialised by
this.a
(the caller),
and
v
by 1. Note that with this approach, recursive method calls are not directly
handled, and require the definition of a fix-point, which we do not consider here.
Search WWH ::
Custom Search