Action:

||||give 5
|||then
||||give the given datum
||and
||||allocate an cell
|||then
||||give it
|then
|||bind "n" to the given cell#2
||and
|||store the given datum#1 in the given cell#2
hence
||unfolding
||||||||||give the datum bound to "n"
|||||||||or
||||||||||give the datum stored in the cell bound to "n"
||||||||then
|||||||||give the given datum
|||||||and
|||||||||give 1
||||||||then
|||||||||give the given datum
||||||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 bound to "temp"
||||||||||||or
|||||||||||||give the datum stored in the cell bound to "temp"
|||||||||||then
||||||||||||give the given datum
||||||||||and
|||||||||||||give the datum bound to "n"
||||||||||||or
|||||||||||||give the datum stored in the cell bound to "n"
|||||||||||then
||||||||||||give the given datum
|||||||||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 bound to "n"
||||||||||||or
|||||||||||||give the datum stored in the cell bound to "n"
|||||||||||then
||||||||||||give the given datum
||||||||||and
||||||||||||give 1
|||||||||||then
||||||||||||give the given datum
|||||||||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 bound to "temp"
|||or
||||give the datum stored in the cell bound to "temp"
||then
|||store the given datum in the cell bound to "n"

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

program while2 =
var n : int := 5
in
while not (n = 1)
do
temp := temp * n;
n := n - 1
end;