Download PIMPL Organizing Files

5.3. PIMPL’s structural operational semantics
Aalborg University
hRule id{Select e; Do S1 , S2 , ... , Sn ; }, envID , sto, envF i −→S
(envID [ id 7→ l], sto[l 7→ (S, ok, (), envID )], envF )
[DCL − R]
where S = ForeachFile I f (e){ S1 S2 ... Sn }
hSDcls , envID , sto, envF i →s henv0ID , sto0 , envF i
hSRules , env0ID , sto0 , envF i →s henv0ID , sto00 , env0F i
hRunRules id1 , ... , idn ; SDcls , envID , sto, envF i →s henv0ID , sto00 , env0F i
[RUNR]
where (sto0 (env0ID id1 ) = (S1 , ok, (), env1ID )) ... (sto(envID idn ) =
(Sn , ok, (), envnID ))
and SRules = S1 S2 ... Sn
Table 5.7. Big-step SOS for Rule and RunRules.
Selector declaration: The transition rule for selector declarations [DCL-S] can be seen in
table 5.8. The transition rule is an axiom which adds a new subprogram to the location l
and updates an envID to map to this location.
Selector call: Here follows an explanation of the [CALL − S] transition rule, for Selector
calls, in table 5.8. Note that a Selector call is an expression, because it results in a value.
The first premise requires that all the syntactic values of the arguments to the Selector can
be converted to actual values.
In the second premise, for the environments envID and envF a statement transition is
performed where statement S is executed and environment env0ID is updated to env00
and
ID
0
envF is updated to envF . envF is updated because the Selector might change the value in
the current file tuple which indicates whether the file is selected or not.
The update of env0ID is a creation of a new scope, and it includes creation of three different
local variables for this new scope. First a variable _IsSelected is created and initialized
to the default Selector return value: ⊥ (false). Secondly a variable _ f ilepath is created
and initialized to the current file’s path which is found in envID . Lastly variables for
all the parameters are created, and the variables are initialized to the parameters actual
values. The statement S, in the second premise, originates from a lookup in the envID
environment, as it can be seen in the first side condition.
_IsSelected is then evaluated to the boolean value bv in the environment env00
from the
ID
resulting state of the transition. This boolean value is the result of the Selector call, which
is reflected in the conclusion of the transition rule.
At the end, in side conditions two, env0F is updated with new information in the current
file, here _IsSelected is set to bv, i.e. if the file was selected.
59