Information Technology Reference
In-Depth Information
Getting values of formal arguments, the value of the current object entity, values of local
variables, the value of the result entity, and attribute values of the current object in a uni-
fied way.
The auxiliary queries
env val
and
att val
define a new auxiliary query
val
that
deals both with values in the top environment as well as with values stored in attributes
of the current object. The auxiliary query
val
takes a processor
p
and a name
n
and it
returns the value of
n
in
p
's current feature execution context. This context consists of
the top environment and its reference to the current object. The auxiliary query requires
that the execution context of processor
p
is setup properly, i.e., there is a top environment
with a reference to the current object. The precondition also states that either the top en-
vironment has the name
n
registered or the current object has an attribute with name
n
.
In any valid SCOOP program, any environment variable has a name that is distinct from
the attribute names of the current object. This allows us to define the result of the auxil-
iary query in a simple way. If the name exists in the top environment, then the result is
the value given by
env val
. Otherwise the name must be the name of an attribute of the
current object, in which case the result is given by
att val
.
val
:
STATE
→
PROC
NAME
REF
∪
PROC
σ
.
val
require
σ
.
regions
.
procs
.
has
(
p
)
¬
σ
.
(
p
,
n
)
store
.
envs
(
p
)
.
is empty
e
)
e
.
names
.
has
(
n
)
∨∃
a
∈
o
.
class type
.
attributes
:
a
.
name
=
n
where
e
de f
.
names
.
has
(
Current
=
σ
.
store
.
envs
(
p
)
.
top
o
de f
=
σ
.
heap
.
ref obj
(
e
.
val
(
Current
))
axioms
⎨
⎩
if e
.
names
.
has
(
n
)
σ
.
env val
(
p
,
n
)
where
e
de f
=
σ
.
store
.
envs
(
p
)
.
top
if
∃
a
∈
o
.
class type
.
attributes
:
a
.
name
=
n
σ
.
att val
(
o
,
n
)
where
e
de f
σ
.
val
(
p
,
n
)=
=
σ
.
store
.
envs
(
p
)
.
top
o
de f
=
σ
.
heap
.
ref obj
(
e
.
val
(
Current
))
Getting values of once functions.
The auxiliary query
is fresh
takes a processor
p
and
a once routine
f
. It returns whether
f
is fresh on
p
or not.
For non-fresh once functions, the auxiliary query
once result
returns the once result
of
f
on
p
.
Locking.
This section explores the aspect of the facade that deals with locking. The
auxiliary query
rq locked
states whether a processor
p
's request queue is locked or
not. There are no auxiliary queries to distinguish between obtained and retrieved locks.
Instead, the auxiliary queries
rq locks
and
cs locks
return the set of all request queue
locks, respectively the set of all call stack locks of a processor
p
. These locks are only
Search WWH ::
Custom Search