The Alma Project, or How First-Order Logic Can Help Us in Imperative Programming - Correct System Design: Recent Insights and Advances - page 101

TYPE Colour = (blue, green, red, yellow);
Info = RECORD
co: Colour;
No: CONSTRAINED INTEGER;
END;
Board = ARRAY [1..M],[1..N] OF Info;
PROCEDURE Region(VAR X: Board; VAR number: INTEGER);
VAR i, j, k: INTEGER;
BEGIN
FORi:=1TOMDO
FORj:=1TONDO
IF i < M AND X[i,j].co = X[i+1,j].co
THEN X[i,j].No = X[i+1,j].No
END;
IF j < N AND X[i,j].co = X[i,j+1].co
THEN X[i,j].No = X[i,j+1].No
END
END
END;
k:=0;
FORi:=1TOMDO
FORj:=1TONDO
IF NOT KNOWN(X[i,j].No)
THEN k := k+1; X[i,j].No = k
END
END
END;
number = k
END Region;
Note that for any i in [1..M] and j in [1..N] , the record component
X[i,j].No is of a constrained type. Here the rst double FOR statement gen-
erates the constraints while the second double FOR statement solves them by
assigning to the pixels that belong to the same region the same number.
Due to the call by variable mechanism, the actual parameter correspond-
ing the formal one, X , is modied by the procedure. In particular, the second
component, No , of each array element is instantiated after the procedure call.
Next, we explain the call by value mechanism in presence of unknowns. An
unknown passed as an actual value parameter is treated as a customary variable:
it is evaluated and its value is assigned to a local variable associated with the
formal parameter. If the value of this unknown is at this moment undetermined,
this evaluation yields a run-time error. This evaluation process also applies if a
eld or an element of a compound actual value parameter is an unknown.