product(_:_:)

head is the correctly rounded value of a*b. If no overflow or underflow occurs, tail represents the rounding error incurred in computing head, such that the exact product is the sum of head and tail computed without rounding.

This operation is sometimes called “twoProd” or “twoProduct”.

Edge Cases:

• head is always the IEEE 754 product a * b.

• If head is not finite, tail is unspecified and should not be interpreted as having any meaning (it may be NaN or infinity).

• When head is close to the underflow boundary, the rounding error may not be representable due to underflow, and tail will be rounded. If head is very small, tail may even be zero, even though the product is not exact.

• If head is zero, tail is also a zero with unspecified sign.

Postconditions:

• If head is normal, then abs(tail) < head.ulp. Assuming IEEE 754 default rounding, abs(tail) <= head.ulp/2.

• If both head and tail are normal, then a * b is exactly equal to head + tail when computed as real numbers.