previous up next
Go backward to Parameterization
Go up to Top
Go forward to Parameter Domains
RISC-Linz logo

Denotation of Parameters

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


Author: Wolfgang Schreiner
Last Modification: December 18, 1997

previous up next