Action:

| | | give 5
| | and 
| | | allocate a cell
| then 
| | | bind "n" to the given cell # 2
| | and 
| | | store (the given integer # 1) in (the given cell # 2)
hence 
| unfolding 
| | | | | | give the integer stored in the cell bound to "n"
| | | | | and 
| | | | | | give 1
| | | | then 
| | | | | give (the given datum # 1) is (the given datum # 2)
| | | then 
| | | | give (not (the given truth-value))
| | then 
| | | | | | check (the given truth-value)
| | | | | and then 
| | | | | | | | | give (the integer 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 integer) in (the cell bound to "n")
| | | | and then 
| | | | | unfold
| | | or 
| | | | check (not (the given truth-value))

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

program dummy =
var n : int := 5
in
while not (n = 1)
do
n := n - 1
end
end