> ideally, a floating-point operations works as though the
> corresponding mathematical operation were performed exactly 
>on the inputs (considered as real numbers), followed by a rounding
> step that takes the resulting real number and rounds it to the 
> nearest floating-point number.

FWIW, the Decimal Arithmetic Specification was created around the same principle.   Accordingly, it gets the answer that Mark expected:

  >>> from decimal import Decimal
  >>> Decimal('-0.5') // Decimal('Inf')
  Decimal('-0')