The array Block is terminated by setting the bit at (Length + 1) to 1
and all following bits to 0.
NOTE: The postcondition currently does not completely express
the intended behaviour of the operation!
derives Block from *,
Length;
pre
Types.Index'First + Types.Index (Length / 64) in Block'Range;
post
(for all I in Types.Index range
Types.Index'First + Types.Index (Length / 64) + 1 .. Block'Last => (Block (I) = 0));