Go backward to Escaping Locations
Go up to Top
Go forward to Declaration Blocks

Extent in Other Block Forms

Declaration block (module)
- module M = begin var A: newint in
  { proc INIT = A:=0,
  proc SUCC = A:=@A+1
  fun VAL = @A
  } end
Location for A is allocated when M is evaluated.
A's location must escape declaration block (body of M)!
- [[pi |- begin D₁ in D₂ end: pi₂dec]] $e$ $s$ =
  [[pi -U- pi₁ |- D₂: pi₂dec]]( $e$ -U- $e$ ₁) $s$ ₁
  where ( $e$ ₁, $s$ ₁) = [[pi |- D₁: pi₁dec]] $e$ $s$
Locations allocated within D₁ and D₂ are retained.

Id: qualification.tex,v 1.2 1996/05/02 11:53:49 schreine Exp schreine