Download PIMPL Organizing Files

Aalborg University
hT id; , envID , sto, envF i −→S
[DCL − VAR]
(envID [id 7→ l], sto[l 7→ De f ault(T)], envF )
[DCL − VAR − INIT]
[DCL − CALC]
[DCL − S]
envID , sto, envF ` e →e allv
hT id = e; , envID , sto, envF i −→S (envID [id 7→ l], sto[l 7→
allv], envF )
hCalculator < T > id(T1 id1 , ... Tn idn ){ S }, envID , sto, envF i −→S
(envID [id 7→ l, sto[l 7→ (S, T, (id1 , ... , idn )], envID )], envF )
0
0
where ∃S ∈ StmtExpand(S) AND S = Result = e;
hSelector id(T1 id1 , ... Tn idn ){ S }, envID , sto, envF i −→S
(envID [ id 7→ l], sto[l 7→ (S, Bool, (id1 , ... , idn ), envID )] envF )
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 }
Table G.11. Operational semantics for declarations.
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 G.12. Big-step SOS transition rules for Rules.
143