Information Technology Reference
In-Depth Information
add obj
:
STATE
→
PROC
OBJ
STATE
σ
.
add obj
(
p
,
o
)
require
σ
.
regions
.
procs
.
has
(
p
)
∀
u
∈
σ
.
heap
.
objs
:
u
.
id
=
o
.
id
∀
a
∈
o
.
class type
.
attributes
:
(
o
.
att val
(
a
)
∈
REF
→
o
.
att val
(
a
)=
void
∨
σ
.
heap
.
refs
.
has
(
o
.
att val
(
a
)))
∧
(
o
.
att val
(
a
)
∈
PROC
→
σ
.
regions
.
procs
.
has
(
o
.
att val
(
a
)))
axioms
σ
.
add obj
(
p
,
o
)=
σ
.
set
(
σ
.
regions
.
add obj
(
p
,
o
)
,
σ
.
heap
.
add obj
(
o
)
,
σ
.
store
)
The auxiliary command
update ref
updates a reference with an updated object. It takes
a reference
r
on the heap and an object
o
and it returns a state in which
o
replaced the
object
u
referenced by
r
on the heap and in the regions. Note that
o
must indeed be
an updated version of the object referenced by
r
. The auxiliary command first removes
u
from the set of handled objects and then adds
o
to the set of handled objects of
u
's
handler. Then it updates the heap with the command
update ref
, which is declared in
HEAP
.
update ref
:
STATE
→
REF
OBJ
STATE
σ
.
require
σ
.
heap
.
refs
.
has
(
r
)
o
.
id
=
σ
.
heap
.
ref obj
(
r
)
.
id
∀
a
∈
o
.
class type
.
attributes
:
(
o
.
att val
(
a
)
∈
REF
→
o
.
att val
(
a
)=
void
∨
σ
.
heap
.
refs
.
has
(
o
.
att val
(
a
)))
∧
(
o
.
att val
(
a
)
∈
PROC
→
σ
.
regions
.
procs
.
has
(
o
.
att val
(
a
)))
axioms
σ
.
update ref
(
r
,
o
)=
σ
.
set
(
k
,
h
,
s
)
where
u
de f
update ref
(
r
,
o
)
=
σ
.
heap
.
ref obj
(
r
)
k
de f
=
σ
.
regions
.
remove obj
(
u
)
.
add obj
(
σ
.
regions
.
handler
(
u
)
,
o
)
h
de f
=
σ
.
heap
.
update ref
(
r
,
o
)
s
de f
=
σ
.
store
Setting values.
This section takes a look at how to set values. To start, it looks at a pre-
requisite for this task: the deep import operation. Setting values includes setting values
of formal arguments, values of local variables, the value of the current object entity, the
value of the result entity, and attribute values of the current object. All of these values
can be written and read without a feature call. This section concludes with auxiliary
commands to set the status of once routines. The SCOOP validity rules exclude other
types of value setting operations.
Deep Import Operation.
Expanded objects have a copy semantics: if an object
o
of
expanded class type is the source of an attachment, then a copy
u
gets attached to the
destination of the attachment. However, a shallow copy is not sufficient if
o
's handler
p
is different from
u
's handler
q
.If
o
has an attached non-separate entity, then
u
now has a
non-separate entity to which a separate object is attached. This would result in a
traitor
- a non-separate entity that points to a separate object. The SCOOP model, as defined
Search WWH ::
Custom Search