Information Technology Reference
In-Depth Information
set val : STATE PROC NAME REF PROC STATE
σ . set val ( p , n , v ) require
σ . regions . procs . has ( p )
¬ σ . store . envs ( p ) . is empty σ . store . envs ( p ) . top . names . has ( Current )
v REF v = void σ . heap . refs . has ( v )
v PROC σ . regions . procs . has ( v )
axioms
if a o . class type . attributes : a . name = n
σ . set att val ( o , n , v )
otherwise
σ . set env val ( p , n , v )
σ . set val ( p , n , v )=
where
o de f
= σ . heap . ref obj ( σ . store . envs ( p ) . top . val ( Current ))
( σ ,
de f
=
v )
if v REF v = void σ . heap . ref obj ( v ) . class type . is exp σ . handler ( v )= p
( σ x , σ x .
last added obj
)
where
σ x de f
= σ . add obj ( p , σ . heap . ref obj ( v ) . copy )
otherwise
( σ , v )
Setting values of once functions. Values can also be stored in the status of once func-
tions. A once function can be fresh or non-fresh. If the once function is non-fresh on a
processor p , then there is a once result for the once function on p . A once function is set
as non-fresh during the execution of the once function. The following discussion takes
a look at how a processor can set the status of once routines in general, i.e., it considers
both once functions and once procedures.
The auxiliary command set once func not fresh takes a processor p , a once function
f , and a value r . It returns an updated state in which f is set as non-fresh with the once
result r .If f is declared as non-separate, then f is set as non-fresh on p with the once
result r .If f is declared as separate with or without an explicit processor specification,
then f is set as non-fresh on all processors.
The auxiliary command set once proc not fresh does the same for once procedures.
It takes a processor p and a once procedure f and it returns a state in which f is set as
non-fresh on p .
Getting values. This section takes a look at how a processor can read a value that got
written with one of the mechanisms from Sec. 4.6.
Getting values of formal arguments, the value of the current object entity, values of
local variables, and the value of the result entity. The auxiliary query envs takes a
processor p and returns the stack of environments for p . The auxiliary query env val
is more specialized. It takes a processor p and a name n and it returns the value stored
under n in the top environment of p .
Getting attribute values of the current object. The auxiliary query att val takes an
object o and a name n and returns the attribute value for the attribute with name n of
object o .
 
Search WWH ::




Custom Search