Action:

| | | give 4 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"))
| | | | | | | | | | | and 
| | | | | | | | | | | | give 1
| | | | | | | | | | then 
| | | | | | | | | | | give ((the given datum # 1) is (the given datum # 2))
| | | | | | | | | then 
| | | | | | | | | | give (the given datum)
| | | | | | | | 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"))
| | | | | | | | | | | | | | and 
| | | | | | | | | | | | | | | give 1
| | | | | | | | | | | | | then 
| | | | | | | | | | | | | | give (difference ( (the given integer # 1) , (the given integer # 2) ))
| | | | | | | | | | | | 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 fact4 =
var x : int := 4;
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