CESK: Class
Note that there are two PITCH rules, one marked as wrong.
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 >
search ends with the return expression (WRONG PITCH)
before:
†
e
s
< [ ], [ ], r >
after:
r
e1
s
pop[ k ]
where
x*, ...
=
all variables of r
and
xl*, ...
=
lookup locations of x* ...
and
e0
=
the environment in the top-most closure
and
e1
=
e0[x* = xl*], ...
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 (success)
before:
(new C x*)
e
s
k
subject to:
class C has the same number of fields as x* has elements
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 (failure)
before:
(new C x*)
e
s
k
subject to:
class C does not have the same number of fields as x* has elements
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
evaluate a field reference (success)
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 (failure)
before:
(o –> f)
e
s
k
subject to:
o may not be an object or does not have the desired field
after:
error
[ ]
[ ]
[ ]
evaluate a method-call expression (success)
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
=
[ ][para* = xl*], ... [this = thisL]
and
s1
=
s[xl* = v*], ... [thisL = obj]
evaluate a method-call expression (failure)
before:
(o –> m (x*))
e
s
k
subject to:
o may not be an object or
... does not have the desired method
... takes a different number of arguments
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 (success)
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 (failure)
before:
v
e
s
< [ ], (o –> f = rhs)::stmt*, r >
subject to:
o may not be an object or does not have the desired field
after:
error
[ ]
[ ]
[ ]