在c#整数运算中，a/b/ C是否总是等于a/(b* C) ?

int a = 5126, b = 76, c = 14;
int x1 = a / b / c;
int x2 = a / (b * c);

我非常喜欢这个问题，我在2013年6月4日把它作为我博客的主题。谢谢你的好问题!

---

大箱子很容易弄到。例如:

a = 1073741823; 
b = 134217727;
c = 134217727;

因为b * c溢出到一个负数。

我要补充的事实是，在检查算术中，a / (b * c)和(a / b) / c之间的差异可以是程序工作和程序崩溃之间的差异。如果b和c的乘积超出整数的边界，则前者将在检查的上下文中崩溃。

对于小的正整数，例如，小到可以放入一个short，则应保持恒等式。

---

Timothy Shields刚刚发布了一个证明;我在这里提出另一种证明。假设这里所有的数字都是非负整数，并且没有运算溢出。

对x / y进行整数除法，得到值q使得q * y + r == x，其中0 <= r < y .

因此除法a / (b * c)找到值q1使得

q1 * b * c + r1 == a

where 0 <= r1 < b * c

除法( a / b ) / c首先找到值qt，使得

qt * b + r3 == a

，然后找到值q2，使得

q2 * c + r2 == qt

把它代入qt得到:

q2 * b * c + b * r2 + r3 == a

where 0 <= r2 < c and 0 <= r3 < b .

两个相等的东西彼此相等，所以我们有

q1 * b * c + r1 == q2 * b * c + b * r2 + r3

假设某整数x对应q1 == q2 + x。代入并求解x:

q2 * b * c + x * b * c + r1 = q2 * b * c + b * r2 + r3
x  = (b * r2 + r3 - r1) / (b * c)

,

 0 <= r1 < b * c
 0 <= r2 < c
 0 <= r3 < b

x可以大于零吗?不。我们有不等式:

 b * r2 + r3 - r1 <= b * r2 + r3 <= b * (c - 1) + r3 < b * (c - 1) + b == b * c

因此该分数的分子总是小于b * c，因此x不可能大于0。

x可以小于零吗?不，以同样的理由，留给读者。

因此整数x为零，因此q1 == q2为零。

设'表示整数除法(c# /在两个int之间的运算符)，设/表示通常的数学除法。那么，如果x,y,z为正整数且忽略溢出，则

(x ' y) ' z
    = floor(floor(x / y) / z)      [1]
    = floor((x / y) / z)           [2]
    = floor(x / (y * z))
    = x ' (y * z)

,

a ' b = floor(a / b)

从上面的[1]行跳转到[2]行解释如下:假设在[0, 1)范围内有两个整数a和b，以及一个小数f。很容易看出

floor(a / b) = floor((a + f) / b)  [3]

如果在[1]行中您识别了a = floor(x / y), f = (x / y) - floor(x / y)和b = z，那么[3]意味着[1]和[2]是相等的。

您可以将此证明推广到负整数(仍然忽略溢出)，但为了使要点简单，我将把它留给读者。

---

关于溢出的问题-请参阅Eric Lippert的回答，以获得很好的解释!在他的博客文章和回答中，他也采取了更严格的方法，如果你觉得我太过挥挥手，你应该看看。

如果b和c的绝对值低于sqrt(2^31)左右(约为。46 300)，这样b * c将永远不会溢出，值将始终匹配。如果b * c溢出，则可以在checked上下文中抛出错误，或者可以在unchecked上下文中获得不正确的值。

避免别人注意到的溢出错误，它们总是匹配的。

让我们假设a/b=q1，这意味着a=b*q1+r1，其中0<=r1<b。
现在假设a/b/c=q2，也就是q1=c*q2+r2，这里的0<=r2<c。
这意味着a=b(c*q2+r2)+r1=b*c*q2+br2+r1 .
为了实现a/(b*c)=a/b/c=q2，我们需要0<=b*r2+r1<b*c。
但是根据需要，b*r2+r1<b*r2+b=b*(r2+1)<=b*c和两个操作匹配。

如果b或c是负的，这不起作用，但我不知道在这种情况下整数除法是如何工作的

为了好玩，我将提供我自己的证明。这也忽略了溢出，不幸的是只处理阳性，但我认为证明是干净而清晰的。

目的是显示

floor(floor(x/y)/z) = floor(x/y/z)

其中/是正除法(贯穿整个证明)。

我们将a/b 的商和余数唯一地表示为a = kb + r(这意味着k,r是唯一的，同时也注意到|r| < |b|)。然后是:

(1) floor(x/y) = k => x = ky + r
(2) floor(floor(x/y)/r) = k1 => floor(x/y) = k1*z + r1
(3) floor(x/y/z) = k2 => x/y = k2*z + r2

所以我们的目标只是显示k1 == k2。我们有:

k1*z + r1 = floor(x/y) = k = (x-r)/y (from lines 1 and 2)
=> x/y - r/y = k1*z + r1 => x/y = k1*z + r1 + r/y

,因此:

(4) x/y = k1*z + r1 + r/y (from above)
x/y = k2*z + r2 (from line 3)

现在从(2)中观察到，r1是一个整数(因为k1*z是定义的整数)，r1 < z(也是定义的整数)。更进一步，从(1)我们知道r < y => r/y < 1。现在考虑(4)中的和r1 + r/y。声明是r1 + r/y < z，这从之前的声明中很明显(因为0 <= r1 < z和r1是整数，所以我们有0 <= r1 <= z-1。因此，0 <= r1 + r/y < z)。因此，r1 + r/y = r2通过r2的定义(否则x/y将有两个余数，这与余数的定义相矛盾)。因此我们有:

x/y = k1*z + r2
x/y = k2*z + r2

，我们得到了我们想要的结论，k1 = k2 .

上面的证明应该与否定一起工作，除了几个步骤，你需要检查一个额外的情况…但我没有检查。

反例:INT_MIN/1/2