Action:

|||||give 0
|||and
|||||allocate a cell
||then
||||bind "count" to the given cell#2
|||and
||||store the given datum#1 in the given cell#2
|before
|||||give 10
|||and
|||||allocate an cell
||then
||||bind "x" 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 "count"
||||and
||||||give 4
|||then
||||give is-less-than(the given datum#1,the given datum#2)
||then
||||||check the given truth-value
|||||and then
||||||||||||give the datum stored in the cell bound to "x"
|||||||||and
|||||||||||give 1
||||||||then
|||||||||give sum(the given integer#1,the given integer#2)
|||||||then
||||||||store the given datum in the cell bound to "x"
||||||and then
||||||||||||give the datum stored in the cell bound to "count"
|||||||||and
|||||||||||give 1
||||||||then
|||||||||give sum(the given integer#1,the given integer#2)
|||||||then
||||||||store the given datum in the cell bound to "count"
||||and then
|||||unfold
|||or
||||check not(the given truth-value)

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

program while1 =
var count : int := 0;
var x : int := 10
in
while (count < 4)
do
x := x + 1;
count := count + 1
end
end