Go backward to Qualification Go up to Top Go forward to Modules

Declaration Blocks

Technical problem

• Scope of [[D₁]] should extend only as far as [[D₂]]
• Additions by D are retained beyond scope of block.

D: Declaration -> Environment -> Store ->
     ((Identifier × Denotable-value)^* × Poststore)

• Denotation of a declaration is list of binding pairs.
• (D[[D]]e s) denotes the bindings defined by [[D]] and not the environment that results when those bindings are added to e.