Left - First input array Right - Second input array Result - Result array
derives
Result from Left, Right;
pre
Left'First = Right'First and
Left'Last = Right'Last and
Right'First = Result'First and
Right'Last = Result'Last;
post
(for all I in Types.Index range Left'First .. Left'Last =>
(Result (I) = XOR2 (Left (I), Right (I))));
Copy all elements of Source to Dest. Should Source be shorter than
Dest, remaining elements stay unchanged.
derives
Dest from *, Source;
pre
Source'First = Dest'First and
Source'Last <= Dest'Last;
post
(for all P in Types.Index range Source'First .. Source'Last =>
(Dest (P) = Source (P)));