带溢出检测的无符号整数乘法算法正确性证明问询

算法代码 #

template<typename UInt> UInt safe_multiply(UInt a, UInt b) {
    UInt x = a * b; // x := ab mod n, n = 2^位数 > 0
    if (a != 0 && x / a != b)
        cerr << "Overflow for " << a << " * " << b << "." << endl;
    return x;
}

严谨证明 #

仅需分析 (a,b,n \in \mathbb{N}_+) 的场景（(a)或(b)为0时无溢出，无需检测）：

假设溢出发生但算法未检测到，即满足两个条件：

1. (ab \geq n)（无符号乘法溢出，结果为 (ab \mod n)）
2. (x / a = b)（算法判断无溢出，其中 (x = ab \mod n)）

根据模运算定义，存在正整数 (k)（因 (ab \geq n)）使得：
[ ab = k \cdot n + x ]

将条件2的 (x = a \cdot b) 代入上式，得：
[ ab = k \cdot n + ab ]

两边消去 (ab) 后得到 (k \cdot n = 0)，但 (k,n) 均为正整数，显然矛盾。因此假设不成立——只要溢出发生，必然有 (x/a \neq b)，算法能100%检测所有溢出。

单行注释版证明（可直接写在代码中） #

// 若ab≥n（溢出），则ab=kn+x(k≥1,x=ab mod n)，若x/a=b则ab=kn+ab→kn=0，与k,n∈ℕ₊矛盾，故溢出时x/a≠b

Codecogs生成的LaTeX图片背景色固定，要根据客户端的深色/浅色模式自动切换，可通过CSS媒体查询实现：

• 生成两张图片URL：分别携带\bg{white}（浅色背景）和\bg{black}（深色背景）参数
• 使用CSS的prefers-color-scheme规则控制显示：

/* 默认显示浅色背景图 */
.latex-light { display: inline-block; }
.latex-dark { display: none; }

/* 深色模式下切换为深色背景图 */
@media (prefers-color-scheme: dark) {
    .latex-light { display: none; }
    .latex-dark { display: inline-block; }
}

• 在HTML中同时引入两张图片：

<img class="latex-light" src="https://latex.codecogs.com/png.latex?\bg{white}你的LaTeX公式内容" alt="公式">
<img class="latex-dark" src="https://latex.codecogs.com/png.latex?\bg{black}你的LaTeX公式内容" alt="公式">

内容的提问来源于stack exchange，提问作者xamid