Go backward to Summary (Syntax) Go up to Top

Summary (Semantics)

• Command block:
  • [[pi |- begin D in C end: comm]]e s =
       free (size-of s) s₂
    where (e₁, s₁) = [[pi |- D: pi₁dec]]e s
    and s₂ = [[pi -U- pi₁ |- C: comm]](e -U- e₁) s₁
• Blocks without storage management:
  • [[pi |-begin D in U end]]e s =
       [[pi -U- pi₁ |- U: theta]]e₁ s₁
    where (e₁, s₁) = [[pi |- D: pi₁dec]]e s
• Copy rule
  • begin define I₁=U₁, ..., define I_n=U_n
    in U end
    => [U₁/I₁, ..., U_n/I_n]U