previous up next
Go backward to Typing Rules
Go up to Top
Go forward to Denotational Semantics
RISC-Linz logo

Denotational Semantics

[[pi |- newint: intloc exp]]e s = allocate s
[[pi |- lazy I=E: { I:theta }exp]]e s =
   ({ I = [[pi |- E:theta]]e }, s)
[[pi |- eager I=E: { I:tau }exp]]e s = ({ I = v }, s')
   where (v, s') = [[pi |- E:tauexp]]e s
[[pi |- I: tauexp]]e s = v s, where (I=v) in e
[[pi |- I: tau]]e s = v, where (I=v) in e
[[pi |- with E1 do E2: theta]]e s =
   [[pi -U- pi1 |- E2: theta]](e -U- [[pi |- E1: pi1]]e) s
[[pi |- with E1 do E2: pi2exp]]e s =
   [[pi -U- pi1 |- E2: pi2exp]](e -U- e1) s1
   where (e1, s1) = [[pi |- E1: pi1exp]]e s
[[pi |- with E1 do E2: store exp]]e s =
   free (size-of s) s2
   where (e1, s1) = [[pi |- E1: pi1exp]]e s
   and s2 = [[pi -U- pi1 |- E2: store exp]](e -U- e1) s1


Author: Wolfgang Schreiner
Last Modification: May 14, 1998

previous up next