
Key: FUML1328

Status: closed

Source: Model Driven Solutions ( Mr. Ed Seidewitz)

Summary:
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

Disposition Summary:
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.

Updated: Thu, 22 Jun 2017 16:38 GMT
FUML13 — The specification of IntegerFunctions::Div is incorrect
 Key: FUML1328
 OMG Task Force: fUML 1.3 RTF