这不是我的作业——我只是在练习。我似乎无法理解这个断言概念。
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}.
【问题讨论】：
标签： c++ assertions preconditions
如果你这样做是为了学习编程，你可以做一些编程来帮助你确认答案：
#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 是浮点数或双精度数，那么在正常的 IEEE 表示中，有一个符号位可以在不影响尾数或指数的情况下切换，从而允许“干净”的符号变化。也就是说，也有“非数字”（NaN）和（正和负）无穷大标记值的极端情况，明智的做法是通过实验和/或通过研究表示和行为规范来检查......
描述为什么 [{ y >= 0 && |y| == |x| }] 比 { y >= 0} 更适合验证代码。
一个模糊的问题，因为我们不确定代码试图实现什么，我们对此的推理循环来自断言前一个后置条件优于后者。尽管如此，他们仍在寻找这样的答案：前者还确保y 的绝对大小在代码对x 所做的符号更改中仍然存在。
在实践中，对于我们的 2 的补码整数，幅度在之后总是匹配 - 它是标记极端情况的后置条件的符号部分。但是，对预期的内容有额外的了解仍然令人放心。
【讨论】：
我猜是因为通常整数类型可以表示 (-N) > 0 > (N-1)。也就是说，如果您的 int 是带符号的 32 位整数，它可以保存值 -2147483648 但不能保存值 2147483648。
{ x != INT_MIN }
【讨论】：
从后置条件向后工作。只有一个分支语句。由于 if 语句测试 x > 0，因此只需查看 3 种情况：x < 0、x == 0 和 x > 0，以确定 x 的哪些值满足后置条件。
【讨论】：
根据x 和y 的类型，这个问题的答案可能会变得混乱。正如@PeteFordham 指出二进制补码中的整数不是对称的，最大负整数的绝对值无法表示。如果不是整数 x 和 y 是 float 或 double 那么你必须考虑在 IEEE 格式中，零可以有正负号。
#include <iostream>
int main() {
double x = 0;
double y = -x;
std::cout << "x=" << x << " y=" << y << std::endl;
}
输出是
x = 0 y = -0
【讨论】：
如果 x > 0，由于if (x > 0) y = x，总是满足 y >= 0。如果 x == 0，由于if ( x > 0) ... else y = -x，总是满足 y >= 0。如果 x = 0 满足，除非 -x = 0 || -x >= 0 }。 （唯一不正确的 x 值是最大负值，它会溢出。）
{ y >= 0 && |y| == |x| } 比 { y >= 0 } 好，因为后者适用于所有类型的函数，而不仅仅是找到 x 的绝对值的函数（这可能是这段代码的用途，尽管您似乎省略了问题陈述）。
【讨论】：