Source: Model Driven Solutions ( Ed Seidewitz)
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).
Reported: FUML 1.2 — Tue, 20 Dec 2016 22:31 GMT
Disposition: Resolved — FUML 1.3
Agreed. In fact, the postcondition also doesn't work, for a similar reason, in the case that both operands are less than zero.
Updated: Thu, 22 Jun 2017 16:38 GMT
FUML13 — The specification of IntegerFunctions::Div is incorrect
- Key: FUML13-28
- OMG Task Force: fUML 1.3 RTF