C++ 前提条件/断言

Question

这不是我的作业——我只是在练习。我似乎无法完全理解这个断言概念。

1) Determine the pre-condition for x that guarantees the post-condition about y
{ _______ }
if (x > 0)
    y = x;
else
    y = -x;

{ y >= 0 && |y| == |x| }
2) This code is the same as has been seen before, but the post-condition is different.                    
Describe why this post-condition is better for verifying the code than just { y >= 0}.

Answer 1

如果你这样做是为了学习编程，你可以做一些编程来帮助你确认答案:

#include <iostream>

int abs(int x) { return x >= 0 ? x : -x; }

int main()
{
    for (int i = -128; i <= 127; ++i)
    {
        char x = i;

        char y;

        if (x > 0)
            y = x;
        else
            y = -x;

        if (!(y >= 0 && abs(y) == abs(x)))
            std::cout << "failed for " << i << " (y " << (int)y << ")\n";
    }
}

运行此程序，您将看到 x -128(其中 y 为 -128)是否失败。这是由于 2 的补码符号的不对称性:-128 可以用 8 位字符表示，但 128 不能(只有 127)。

因此对于 1，并假设 2 的补整数，前提是 x 不是您的位宽中的最低可表示值。当然，问题中没有任何内容说 x 和 y 甚至是整数，所以它有点试探性。

如果 x 和 y 是 float 或 double ，那么在正常的 IEEE 表示中有一个符号位可以切换而不影响尾数或指数，允许“干净”的标志变化。也就是说，也有“不是数字”(NaN)和(正和负)无穷大哨兵值的极端情况，明智的做法是通过实验和/或研究表示和行为规范来检查……

Describe why [{ y >= 0 && |y| == |x| }] is better for verifying the code than just { y >= 0}.

一个模糊的问题，因为我们不确定代码试图实现什么，我们对此的推理循环地来自前一个后置条件优于后者的断言。尽管如此，他们仍在寻找这样的答案:前者还确保​​ y 的绝对大小在代码对 x 所做的任何符号更改中仍然存在。

在实践中，对于我们的 2 的补码整数，其大小总是在之后匹配 - 它是标记极端情况的后置条件的符号部分。但是，对预期的内容有额外的了解仍然令人放心。