Download reusable_components_..

DESCRIPTION OF LIBRARY MACHINES
31
5.3 L ARRAY3: Array with Non Ordered Values, Maximum Operations
OPERATIONS
VAL ARRAY
value of an element (promoted operation).
STR ARRAY
write an element (promoted operation).
SET ARRAY
write the same value in an array portion (promoted operation).
SWAP ARRAY
exchange two elements (promoted operation).
RIGHT SHIFT ARRAY shift a portion to the main index (promoted operation).
LEFT SHIFT ARRAY shift a portion to the small index (promoted operation).
SEARCH MAX EQL ARRAY search for a value in an array (promoted operation).
SEARCH MIN EQL ARRAY search for a value in an array portion (promoted operation).
REVERSE ARRAY reverse the order of elements in an array portion.
EXAMPLE
The example below is a machine that represents the color assigned to 101 points, this color
may be red, green or blue for each point. An operation is used to find a red dot.
MACHINE
m1
SETS
COLOR = {red, green, blue}
VARIABLES
color
INVARIANT
color ∈ 0. .100 → COLOR
INITIALISATION
color :=(0. .100) ×{red}
OPERATIONS
ii,bb ← trouve red = pre
rouge ∈ ran(color)
then
ii :∈ color−1 [{red}] ||
bb :∈ BOOL
end
END
IMPLEMENTATION
m1 1
REFINES
m1
IMPORTS
i1.L ARRAY3(COLOR,100)
INVARIANT
i1.arr vrb = color
INITIALISATION
i1.SET ARRAY(0,100,red)
OPERATIONS
ii,bb ← trouve red =
var bb in
ii,bb ←
i1.SEARCH MAX EQL ARRAY(0,100,red)
end
END
DESCRIPTION
L ARRAY3 is the most complete of the one dimensional array machines that do not
require that the output set be part of an interval. L ARRAY5 has been constrained. It
is therefore possible to create arrays with values that are elements of a listed set while
having access to complete operations such as element order reversal. The operation that