5 —
Due Thursday, 09 October 2025, 11:59:59pm
Purpose to build a semantic model for a language with lexically scoped variables
Delivery Deliver your solutions in a directory called 5 within your assigned GitHub repository. The directory should contain the following items:
the executables xcesk as specified below;
the sub-directory 5/Tests/ with the required integration test; and
an optional sub-directory called 5/Other/ for all auxiliary files.
load, which consumes an AST of a Core program (see 4 —
Core: Validity) and constructs an initial CESK state; transition, which consumes a non-final CESK state and constructs the next state as specified in figure 7; and
unload, which consumes a final CESK state and returns an answer: a number or an informative error message.
C contains a control string, which is either a † (pronounced “I am searching for an expression”) token or a Core expression.
E contains an “environment”, which associates variables with Locations.
S contains a “store”, which associates Locations with numbers.
K contains the rest of the instructions that the machine must execute once the expression in C is evaluated. It is represented as a stack of closures. Each closure corresponds to a nested block, and the bottom-most one represents the “root” of the program.
An initial state contains † in C, empty associations in E and S, and a stack frame with the given program AST in K.
A final state contains a number in C and empty stack in K.
A closure combines a program AST with an environment. The AST represents the remaining instructions of either the top-most program (bottom-most stack frame) or a nested block (all others); if the AST represents a nested block, the expression field is filled with a dummy value. The environment represents the meaning of variables in the surrounding context.
The set of Locations is an infinitely large set of arbitrary values. Here “infinite” means that, give some finite collection of locations, an algorithm can create a new one.
Exercise Design the CESK transition for the comparison expression (Variable == Variable). Its purpose is to compare the current values of the two variables.
| x – y | < ϵ
The rule ``search encounters nested block'' has been updated.
In the following tables, < def*, stmt*, r > is notation for a stack whose top-most frame contains the block consisting of def*, a potentially empty sequence of definitions; stmt*, a potentially empty sequence of statements; and r, a return expressions (which may just be $). The notation f::others denotes a sequence with at least one element f, followed by a potentially empty sequences of others of the same kind.
Blocks and Definitions
Control
Environment
Store
Kontinuation
search ends with def rhs
before:
†
e
s
< (def x rhs)::def*, stmt*, r >
after:
rhs
e
s
< (def x rhs)::def*, stmt*, r >
value for 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 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 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
before:
†
e
s
< [ ], [ ], r >
after:
r
e
s
< [ ], [ ], r >
search ends with evaluated return expression
before:
v
e
s
< [ ], [ ], r >
after:
v
e1
s
pop[ k ]
where
e1
=
the environment in the top-most closure
and
k
=
< [ ], [ ], r >
Control
Environment
Store
Kontinuation
evaluate a variable
before:
y
e
s
k
after:
n
e
s
k
where
yl
=
e[y]
and
n
=
s[yl]
evaluate an addition
before:
(y + z)
e
s
k
after:
+
e
s
k
where
yl
=
e[y]
and
zl
=
e[z]
and
yn
=
s[yl]
and
zn
=
s[zl]
evaluate a division (success)
before:
(y / z)
e
s
k
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)
before:
(y / z)
e
s
k
subject to:
z is 0.0
after:
error
e
s
[ ]
Control
Environment
Store
Kontinuation
search ends with right-hand side of assignment
before:
†
e
s
< [ ], (x = rhs)::stmt*, r >
after:
rhs
e
s
< [ ], (x = rhs)::stmt*, r >
value for right-hand side of assignment
before:
n
e
s
< [ ], (x = rhs)::stmt*, r >
after:
†
e
s[xl = n]
< [ ], stmt*, r >
where
xl
=
e[x]
Control
Environment
Store
Kontinuation
search for expression in while
before:
†
e
s
< [ ], (while0 tst body)::stmt*, r >
after:
tst
e
s
< [ ], (while0 tst body)::stmt*, r >
decide whether to run 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 while loop (negative)
before:
n
e
s
< [ ], (while0 tst body)::stmt*, r >
subject to:
n is not 0.0
after:
†
e
s
< [ ], stmt*, r >
Control
Environment
Store
Kontinuation
search for expression in if
before:
†
e
s
< [ ], (if0 tst thn els)::stmt*, r >
after:
tst
e
s
< [ ], (if0 tst thn els)::stmt*, r >
pick then branch from if0
before:
n
e
s
< [ ], (if0 tst thn els)::stmt*, r >
subject to:
n is 0.0
after:
†
e
s
< [ ], thn::stmt*, r >
pick else branch from if0
before:
n
e
s
< [ ], (if0 tst thn els)::stmt*, r >
subject to:
n is not 0.0
after:
†
e
s
< [ ], els::stmt*, r >
Figure 7: The CESK semantics of the Core language: transition function
The xcesk program reads one ExampleCC from STDIN, constructs the AST, checks its validity, runs the CESK machine on it, and writes one of the following strings to STDOUT: The outcomes are listed in the order in which they may occur for a given program.
"parser error" if the given ExampleCC is not an element of the Core grammar;
"undeclared variable error" if in the well-formed Core program one of its variable occurrences comes without declaration;
a number n if the CESK machine produces a number n for the well-formed and valid Core program;
"run-time error" if the CESK machine produces an error outcome for the well-formed and valid Core program.
Testing Task Create 10 integration tests for xcesk.
A test always consists of inputs, expected
output, and an automated procedure for comparing the actual output
with the expected one. —
Readings Nested Blocks (CESK)