Information Technology Reference
In-Depth Information
are implicitly taken care of because no change to the state is necessary. The result is the
state
σ
y
.
The last step defines the result of the function, based on the definitions of the preced-
ing steps. The result generation step defines the resulting reference
r
to the imported
object
o
n
, the resulting map
w
, and the resulting state
σ
.
deep import rec without map
(
p
,
q
,
r
,
w
,
σ
)=(
r
,
w
,
σ
)
where
o
de f
=
σ
.
ref obj
(
r
)
o
0
de f
=
o
.
copy
σ
0
de f
σ
.
add obj
(
p
,
o
0
)
if
σ
.
handler
(
r
)=
q
σ
.
add obj
(
σ
.
handler
(
r
)
,
o
0
)
otherwise
=
w
0
de f
=
w
.
add
(
r
,
σ
0
.
ref
(
o
0
))
{
a
1
,...,
a
n
}
de f
=
{
a
|
o
.
att val
(
a
)
∈
REF
∧
o
.
att val
(
a
)
=
void
}
de f
=
r
i
,
w
i
,
σ
i
)
w
i
−
1
,
σ
i
−
1
)
∀
i
∈{
1
,...,
n
}
:
(
deep import rec with map
(
p
,
q
,
o
.
att val
(
a
i
)
,
de f
=
o
i
−
1
.
set att val
(
a
i
,
r
i
)
∀
i
∈{
1
,...,
n
}
:
o
i
σ
x
de f
=
σ
n
.
update ref
(
σ
n
.
ref
(
o
0
)
,
o
n
)
σ
y
de f
=
σ
x
.
set once func not fresh
(
σ
x
.
handler
(
σ
x
.
ref
(
o
n
))
,
f
1
,
σ
x
.
once result
(
σ
x
.
handler
(
r
)
,
f
1
))
. ...
.
set once func not fresh
(
σ
x
.
handler
(
σ
x
.
ref
(
o
n
))
,
f
w
,
σ
x
.
once result
(
σ
x
.
handler
(
r
)
,
f
w
))
.
set once proc not fresh
(
σ
x
.
handler
(
σ
x
.
ref
(
o
n
))
,
f
w
+
1
)
. ...
.
set once proc not fresh
(
σ
x
.
handler
(
σ
x
.
ref
(
o
n
))
,
f
m
)
where
{
x
∈
o
.
class type
.
functions
|
x
.
is once
∧∃
c
,
d
: Γ
x
:
(
d
, •,
c
)
∧
σ
x
.
is fresh
(
σ
x
.
handler
(
σ
x
.
ref
(
o
n
))
,
x
)
∧
¬
σ
x
.
is fresh
(
σ
x
.
handler
(
r
)
,
x
)
}
de f
=
{
f
1
,...,
f
w
}
{
x
∈
o
.
class type
.
procedures
|
x
.
is once
∧
de f
=
σ
x
.
(
σ
x
.
(
σ
x
.
o
n
))
,
{
f
w
+
1
,...,
f
m
}
is fresh
handler
ref
(
x
)
∧
¬
σ
x
.
is fresh
(
σ
x
.
handler
(
r
)
,
x
)
}
de f
=
σ
y
.
ref
(
o
n
)
r
de f
=
w
n
σ
de f
w
=
σ
y
Setting values of formal arguments and the value of the current object entity.
The deep
import operation is used in two ways. It is used when an expanded object handled by
one processor gets used as an actual argument for a formal argument on another pro-
cessor. The deep import operation also gets used when an expanded object handled by
one processor gets returned to another processor. This section focuses on the argument
passing aspect.
The auxiliary command
push env with feature
defines a state in which a processor
p
receives a new environment. The new environment is initialized for the execution of
the feature
f
with target reference
r
0
and actual argument references
.Actual
arguments of expanded type must either be copied or they must be deep imported.
(
r
1
,...,
r
n
)
Search WWH ::
Custom Search