Action:

|||||give 5
|||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 "fact" to closure abstraction of
||||||rebind
|||||moreover
||||||bind "n" to the given cell
||||hence
|||||||rebind
||||||moreover
||||||||||give 1
||||||||and
||||||||||allocate a cell
|||||||then
|||||||||bind "temp" to the given cell#2
||||||||and
|||||||||store the given datum#1 in the given cell#2
|||||hence
|||||||unfolding
|||||||||||||||give the datum stored in the cell bound to "n"
|||||||||||then
||||||||||||give (the given datum#1 is 1)
|||||||||then
||||||||||give not(the given truth-value)
||||||||then
||||||||||||check the given truth-value
|||||||||||and then
||||||||||||||||||give the datum stored in the cell bound to "temp"
|||||||||||||||and
||||||||||||||||||give the datum stored in the cell bound to "n"
||||||||||||||then
|||||||||||||||give product(the given integer#1,the given integer#2)
|||||||||||||then
||||||||||||||store the given datum in the cell bound to "temp"
||||||||||||and then
||||||||||||||||||give the datum stored in the cell bound to "n"
||||||||||||||then
|||||||||||||||give difference(the given integer#1,1)
|||||||||||||then
||||||||||||||store the given datum in the cell bound to "n"
||||||||||and then
|||||||||||unfold
|||||||||or
||||||||||check not(the given truth-value)
||||||and then
|||||||||give the datum stored in the cell bound to "temp"
|||||||then
||||||||store the given datum in the cell bound to "n"
hence
||give the cell bound to "x"
|then
||enact application (the abstraction bound to "fact") to (the given datum)

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

program fact5 =
var x : int := 5;
proc fact (var n : int) =
local
var temp : int := 1
in
while not (n = 1)
do
temp := temp * n;
n := n - 1
end;
n := temp
end
end
in
fact (var x)
end