严格证明以下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)规范.

第一:我不能以正式的方式陈述财产.

形式化版本可以是:对于每个语句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

在我看来，最简单的解决方案就是向后证明这一点。如果 的第一个参数f是最大参数，则证明返回第一个参数（相当简单 -a根据定义，最大参数大于b）。如果第二个参数是最大参数，则证明第二个参数被返回。如果两者相等，则表明不存在唯一的最大元素，因此第二个参数仍然是最大参数。

最后，证明这三个选项是详尽的。如果传递唯一的最大参数，则必须将其作为第一个或第二个参数传递，因为f它是二进制的。