c++ - 以下 C++ 代码的属性的严格证明？

Question

采用以下 C++14 代码片段:

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

声明: 函数 f 返回其参数的最大值。

现在，该陈述“显然”是正确的，但我未能根据 ISO/IEC 14882:2014(E) 规范严格证明它。

首先:我不能以正式的方式陈述属性(property)。

正式版本可以是:对于每个语句 s，当抽象机(在规范中定义)处于状态 P 并且 s 看起来像“f( expr_a,expr_b)"和 s 中的 'f' 被解析为有问题的函数，s(P).return= max(expr_a(P).return, expr_b(P).return).

这里对于状态 P 和表达式 s，s(P) 是机器在评估 s 之后的状态。

问题什么是该陈述的正确形式化版本？如何使用上述规范强加的属性来证明该陈述？对于每个推导步骤，请引用允许所述步骤的标准中的适用片段(片段数量足够)。

编辑:可能在 Coq 中形式化

Answer 1

请原谅我大概老化的数学知识。

自然数 (BN) 的闭子集的最大值可以定义如下:

Max:(BN,BN) -> BN
(x ∊ BN)(a ∊ BN)(b ∊ BN)(x = Max(a,b)) => ( x=a & a>b | x=b )

符号具有共同的数学意义。

虽然您的函数可以重写如下，其中 UN 是 unsigned int 的集合:

f:(UN,UN) -> UN
(x ∊ UN)(a ∊ UN)(b ∊ UN)(x = f(a,b)) => ( x=a && a>b || x=b )

其中符号 = 是 operator==(unsigned int,unsigned int) 等...

因此，问题简化为了解标准是否指定由 unsigned integer 与 C++ 算术运算符和比较运算符形成的数学结构同构到由具有公共(public)算术运算和关系的 N 的封闭子集形成的数学结构(类、类别)。我认为答案是肯定的，这是用简单的英语表达的:

C++14 标准，[expr.rel]/5 (关系运算符)

If both operands (after conversions) are of arithmetic or enumeration type, each of the operators shall yield true if the specified relationship is true and false if it is false.

C++14 标准，[basic.fundamental]/4 (基本类型)

Unsigned integers shall obey the laws of arithmetic modulo 2n where n is the number of bits in the value representation of that particular size of integer.

那么你也可以证明 ({true,false},&&,||) 是通过分析 [expr.log.and] 中的文本也与 bool 算术同构 和 [expr.log.or]

---

我认为除了证明存在这种同构之外，您不应该走得更远，因为走得更远意味着证明公理。