FUML13 — The specification of IntegerFunctions::Div is incorrect

Consider an application of IntegerFunctions::Div(x,y) when x > 0 but y < 0. In this case, the postcondition in the definition of the function (given in 9.3.2, Table 9.3) requires that -Div(x,y) * y <= -x < (-Div(x,y) + 1) * y. But this is impossible, because (-Div(x,y) + 1) * y < -Div(x,y) * y, since y < 0.

The "else" expression in the postcondition should actually be:
((Neg(result) * Abs(y)) <= Abs(x) And ((Neg(result)+1) * Abs(y) > Abs(x)
This would ensure that Div(x,y) = -Div(-x,y) = -Div(x,-y) = Div(-x,-y), for all values of x and y (with y <> 0).

Correct postcondition

Agreed. In fact, the postcondition also doesn't work, for a similar reason, in the case that both operands are less than zero.