Go backward to Parameterization Go up to Top Go forward to Parameter Domains |
Abstract with body [[V]] and parameters [[I1]] ...[[In]] has denotation of form
(lambda p1. ...lambda pn. V[[V]] ...)
D ::= ...| proc I1(I2) = C
C ::= C1; C2 | ...| I(E)
Proc = Param -> Store ->
Poststore_|_
D[[proc I1(I2) = C]] = lambda e.lambda s.
((updateenv [[I1]]
inProc(lambda a. C[[C]](updateenv
[[I2]] a e)) e),
(return s))
C[[I(E)]] = lambda e.lambda s.
cases (accessenv [[I]]
e) of
isNatlocn(I) -> (signalerr s)
...
[] isProc(q) -> (q (...E[[E]]
...) s)
end