Action:

|||||give 0
|||and
|||||allocate a cell
||then
||||bind "x" to the given cell#2
|||and
||||store the given datum#1 in the given cell#2
|before
||recursively bind "inc" to closure abstraction of
||||||rebind
|||||moreover
||||||bind "y" to the given datum
||||hence
||||||||||give the datum bound to "y"
|||||||and
|||||||||give 10
||||||then
|||||||give sum(the given integer#1,the given integer#2)
hence
|||give 1
||then
|||enact (application (the abstraction bound to "inc") to (the given datum))
|then
||store the given datum in the cell bound to "x"

The above action is the meaning of the following Specimen program:

program inc3 =
var x : int := 0;
fun inc y : int -> int = y + 10
in
x := inc (1)
end