如何基于C++14标准严谨证明指定函数的取最大值特性？

原C++14代码片段 #

先看用户提供的目标函数：

unsigned int f(unsigned int a, unsigned int b){ 
  if(a>b)return a; 
  return b; 
}

核心困惑 #

这个函数看起来显然是返回两个无符号整数参数的最大值，但要基于ISO/IEC 14882:2014(E)（C14标准）做严谨证明时，首先卡壳的是如何把自然语言的命题转化为严格的形式化表述——毕竟“返回参数的最大值”这种说法，在形式化逻辑里需要精准对应C无符号整数的语义规则。

命题的正确Coq形式化表述 #

我们可以用Coq来精准映射C++无符号整数的行为，把命题转化为可验证的逻辑语句：

(* 建模C++ unsigned int：模2^w的无符号整数，w为类型位数 *)
Parameter uint : Type.
Parameter uint_eq : uint -> uint -> Prop.
Parameter uint_gt : uint -> uint -> Prop.
Parameter uint_max : uint -> uint -> uint.

(* 定义C++无符号整数最大值的语义：匹配比较规则的分支逻辑 *)
Axiom max_def : forall a b : uint,
  (uint_gt a b -> uint_eq (uint_max a b) a) /\
  (~uint_gt a b -> uint_eq (uint_max a b) b).

(* 形式化函数f的行为等价于uint_max *)
Theorem f_returns_max : forall a b : uint,
  let f (a b : uint) := if uint_gt a b then a else b in
  uint_eq (f a b) (uint_max a b).

这个形式化完全贴合C++无符号整数的比较与取值规则，把“返回最大值”转化为了基于逻辑分支的等价命题。

基于C++14标准的严谨证明 #

下面每一步都对应标准条款，做合规性推导：

步骤1：明确unsigned int的基础语义 #

对应标准条款：3.9.1p4（无符号整数类型）
无符号整数类型的对象能表示0到2^{N-1的数值（N为类型位数），算术运算遵循模2}N规则，比较运算直接基于二进制数值的大小（无符号扩展）。

步骤2：解析a>b的判定逻辑 #

对应标准条款：5.9p2（关系运算符）
对于无符号整数操作数，>运算符返回true当且仅当左操作数的数值严格大于右操作数；否则返回false。这和我们形式化中uint_gt`的定义完全一致。

步骤3：解析return语句的行为 #

对应标准条款：6.6.3p2（return语句）
return语句会将指定值作为函数返回值传递给调用者，并终止函数执行。因此当a>b为true时，函数返回a；否则返回b。

步骤4：关联到“最大值”的定义 #

对应标准依据：基于3.9.1p4的数值定义推导
对于两个无符号整数a和b，它们的最大值max(a,b)的自然定义就是：若a数值大于b则取a，否则取b。这完全匹配函数f的分支逻辑。

最终结论 #

结合以上所有标准条款的推导，函数f的行为完全符合无符号整数最大值的定义，命题成立。

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