CESK: Mixed
Blocks and Declarations
Control
Environment
Store
Kontinuation
search ends with the rhs of a declaration
before:
†
e
s
< (def x rhs)::def*, stmt*, r >
after:
rhs
e
s
< (def x rhs)::def*, stmt*, r >
value found for the right-hand side of declaration
before:
n
e
s
< (def x rhs)::def*, stmt*, r >
after:
†
e[x = xl]
s[xl = n]
< def*, stmt*, r >
where
xl
=
a new (relative to s) location
search encounters a nested block
before:
†
e
s
< [ ], (block d* s*)::stmt*, r >
after:
†
e
s
push[ cl, k ]
where
k
=
< [ ], stmt*, r >
and
cl
=
closure: (d* s* $) in e
search exhausts a nested block
before:
†
e
s
< [ ], [ ], $ >
after:
†
e1
s
pop[ k ]
where
e1
=
the environment in the top-most closure
and
k
=
< [ ], [ ], $ >
search ends with the return expression (PITCH)
before:
†
e
s
< [ ], [ ], r >
after:
r^
e1
s1
pop[ k ]
where
z*, ...
=
all variables of r
and
v*, ...
=
s[e[ z* ]], ...
and
r^
=
rename all variables of r to unique names
and
x*, ...
=
all variables of r^
and
xl*, ...
=
as many new (relative to s) locations as elements in x*, ...
and
e0
=
the environment in the top-most closure
and
e1
=
e0[x* = xl*], ...
and
s1
=
s[xl* = v*], ...
and
k
=
< [ ], [ ], r >
Control
Environment
Store
Kontinuation
search ends with the right-hand side of an assignment
before:
†
e
s
< [ ], (x = rhs)::stmt*, r >
after:
rhs
e
s
< [ ], (x = rhs)::stmt*, r >
value found for the right-hand side of an assignment
before:
n
e
s
< [ ], (x = rhs)::stmt*, r >
after:
†
e
s[xl = n]
< [ ], stmt*, r >
where
xl
=
e[x]
search for an expression in a while loop
before:
†
e
s
< [ ], (while0 tst body)::stmt*, r >
after:
tst
e
s
< [ ], (while0 tst body)::stmt*, r >
decide whether to run the while loop (positive)
before:
n
e
s
< [ ], (while0 tst body)::stmt*, r >
subject to:
n is 0.0
after:
†
e
s
< [ ], body::o, r >
where
o
=
(while0 tst body)::stmt*
decide whether to run the while loop (negative)
before:
n
e
s
< [ ], (while0 tst body)::stmt*, r >
subject to:
n is not 0.0
after:
†
e
s
< [ ], stmt*, r >
search for expression in a conditional
before:
†
e
s
< [ ], (if0 tst thn els)::stmt*, r >
after:
tst
e
s
< [ ], (if0 tst thn els)::stmt*, r >
pick the ‘then‘ branch of a conditional
before:
n
e
s
< [ ], (if0 tst thn els)::stmt*, r >
subject to:
n is 0.0
after:
†
e
s
< [ ], thn::stmt*, r >
pick the ‘else‘ branch of a conditional
before:
n
e
s
< [ ], (if0 tst thn els)::stmt*, r >
subject to:
n is not 0.0
after:
†
e
s
< [ ], els::stmt*, r >
Control
Environment
Store
Kontinuation
evaluate a number
before:
n
e
s
k
after:
n
e
s
k
evaluate a variable
before:
y
e
s
k
after:
n
e
s
k
where
yl
=
e[y]
and
n
=
s[yl]
evaluate an addition (success)
before:
(y + z)
e
s
k
subject to:
y and z are numbers
after:
+
e
s
k
where
yl
=
e[y]
and
zl
=
e[z]
and
yn
=
s[yl]
and
zn
=
s[zl]
evaluate an addition (failure)
before:
(y + z)
e
s
k
subject to:
y or z is not a number
after:
error
[ ]
[ ]
[ ]
evaluate a comparison
before:
(y == z)
e
s
k
after:
rr
e
s
k
where
yl
=
e[y]
and
zl
=
e[z]
and
yn
=
s[yl]
and
zn
=
s[zl]
and
rr
=
are yn and zn structurally equal?
evaluate a division (success)
before:
(y / z)
e
s
k
subject to:
y and z are numbers
subject to:
z is not 0.0
after:
double ieee division of yn by zn
e
s
k
where
yl
=
e[y]
and
zl
=
e[z]
and
yn
=
s[yl]
and
zn
=
s[zl]
evaluate a division (failure: division by 0)
before:
(y / z)
e
s
k
subject to:
y and z are numbers
subject to:
z is 0.0
after:
error
[ ]
[ ]
[ ]
evaluate a division (failure: one operand is not a number)
before:
(y / z)
e
s
k
subject to:
y or z is not a number
after:
error
[ ]
[ ]
[ ]
Control
Environment
Store
Kontinuation
evaluate a ‘new‘ expression (untyped class, success)
before:
(new C (x* ...))
e
s
k
subject to:
untyped class C has the same number of fields as in x* ...
after:
obj
e
s
k
where
v*
=
s[e[ x* ]], ...
and
obj
=
create instance of C using v*, ... for the values of the fields
evaluate a ‘new‘ expression (typed class, success)
before:
(new C (x* ...))
e
s
k
subject to:
typed class C has the same number of fields as in x* ...
after:
prx
e
s
k
where
v*, ...
=
s[e[ x* ]], ...
and
obj
=
create instance of C using v*, ... for the values of the fields
and
typ
=
the type of the class
and
prx
=
make value conform to type
evaluate a ‘new‘ expression (failure)
before:
(new C (x* ...))
e
s
k
subject to:
class C does not have the same number of fields as in x* ...
after:
error
[ ]
[ ]
[ ]
evaluate an ‘isa‘ expression
before:
(o isa C)
e
s
k
after:
ans
e
s
k
where
obj
=
s[e[ o ]]
and
ans
=
check whether obj is instance of C
Control
Environment
Store
Kontinuation
evaluate a field reference (object)
before:
(o –> f)
e
s
k
subject to:
o is an object and has the desired field
after:
ans
e
s
k
where
obj
=
s[e[ o ]]
and
ans
=
get value of f from obj
evaluate a field reference (proxy)
before:
(p –> f)
e
s
k
subject to:
p is a proxy and its field type matches
after:
v
e
s
k
where
prx
=
s[e[ p ]]
and
[ obj, fieldType ]
=
extract object and type of f from proxy
and
u
=
get value of f from obj
and
v
=
make value conform to field type
evaluate a field reference (failure)
before:
(o –> f)
e
s
k
subject to:
o is not be an object/proxy with the right field property
after:
error
[ ]
[ ]
[ ]
where
obj
=
s[e[ o ]]
Control
Environment
Store
Kontinuation
evaluate a method-call expression (object)
before:
(o –> m (x* ...))
e
s
k
subject to:
o is an object
... has the desired method
... the correct number of parameters
after:
†
e1
s1
push[ cl, k ]
where
obj
=
s[e[ o ]]
and
v*, ...
=
s[e[ x* ]], ...
and
[ para*, body ]
=
the parameters & body of method m inthe class of obj
and
cl
=
closure: body in e
and
thisL
=
a new (relative to s) location
and
xl*, ...
=
as many new (relative to s) locations as elements in x*, ...
and
e1
=
[ ][this = thisL][para* = xl*], ...
and
s1
=
s[thisL = obj][xl* = v*], ...
evaluate a method-call expression (proxy)
before:
(p –> m (x* ...))
e
s
k
subject to:
p is a proxy and its method type matches
after:
†
e1
s1
push[ cl, push[ rangeT, k ] ]
where
prx
=
s[e[ p ]]
and
[ obj, domainT, rangeT ]
=
extract object and method type from proxy
and
tmp*, ...
=
s[e[ x* ]], ...
and
arg*, ...
=
make tmp* ... conform to domain types
and
[ para*, body ]
=
the parameters & body of method m inthe class of obj
and
cl
=
closure: body in e
and
thisL
=
a new (relative to s) location
and
xl*, ...
=
as many new (relative to s) locations as elements in x*, ...
and
e1
=
[ ][this = thisL][para* = xl*], ...
and
s1
=
s[thisL = obj][xl* = arg*], ...
evaluate a method-call expression (failure)
before:
(o –> m (x*))
e
s
k
subject to:
o is not be an object/proxy with the right properties for this call
after:
error
[ ]
[ ]
[ ]
returning from a proxied method call (success)
before:
v
e
s
(type: rangeT)::k
subject to:
value type matches rangeT
after:
rv
e
s
k
where
rv
=
make value conform to range type
returning from a proxied method call (failure)
before:
v
e
s
(type: rangeT)::k
subject to:
value type does not match rangeT
after:
error
[ ]
[ ]
[ ]
Control
Environment
Store
Kontinuation
search ends a field assignment
before:
†
e
s
< [ ], (o –> f = rhs)::stmt*, r >
after:
rhs
e
s
< [ ], (o –> f = rhs)::stmt*, r >
execute a field assignment (object)
before:
v
e
s
< [ ], (o –> f = rhs)::stmt*, r >
subject to:
o is an object and has the desired field
after:
†
e
s
< [ ], stmt*, r >
where
obj
=
s[e[ o ]]
and
set f in obj to v
execute a field assignment (proxy)
before:
u
e
s
< [ ], (p –> f = rhs)::stmt*, r >
subject to:
p is a proxy and its field type matches
after:
†
e
s
< [ ], stmt*, r >
where
prx
=
s[e[ p ]]
and
[ obj, fieldT ]
=
extract object and type of f from proxy
and
v
=
make value conform to field type
and
set f in obj to v
execute a field assignment (failure)
before:
v
e
s
< [ ], (o –> f = rhs)::stmt*, r >
subject to:
o is not be an object/proxy with the right field property
after:
error
[ ]
[ ]
[ ]
where
obj
=
s[e[ o ]]
Figure 30: The proxy-based CESK machine: transition function