2

这不是我的作业——我只是在练习。我似乎无法围绕这个断言概念来思考。

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}.
4

5 回答 5

2

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

#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";
    }
}

运行这个你会看到 -128 是否失败x（其中y是 -128）。这是由于 2 的补码表示法的不对称性：-128 可以用 8 位字符表示，但 128 不能（只有 127）。

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

如果xandy是浮点数或双精度数，那么在正常的 IEEE 表示中，有一个符号位可以在不影响尾数或指数的情况下进行切换，从而允许符号的“干净”变化。也就是说，也存在“非数字”（NaN）和（正和负）无穷大标记值的极端情况，明智的做法是通过实验和/或通过研究表示和行为规范来检查......

描述为什么 [{ y >= 0 && |y| == |x| }] 比 { y >= 0} 更适合验证代码。

一个模糊的问题，因为我们不确定代码试图实现什么，我们对此的推理循环来自断言前一个后置条件优于后者。尽管如此，他们仍在寻找这样的答案：y无论代码对x.

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

于 2013-02-28T04:51:39.610 回答
1

我猜是因为通常整数类型可以表示 (-N) > 0 > (N-1)。也就是说，如果您的 int 是带符号的 32 位整数，它可以保存值 -2147483648，但不能保存值 2147483648。

{ x != INT_MIN }

于 2013-02-28T04:33:53.663 回答
0

从后置条件向后工作。只有一个分支语句。由于 if 语句测试 x > 0 ，因此只需查看 3 种情况：x < 0、x == 0和x > 0来确定 x 的哪些值满足后置条件。

于 2013-02-28T04:28:54.617 回答
0

如果 x > 0，由于 . 总是满足 y >= 0 if (x > 0) y = x。如果 x == 0，由于 .y >= 0 总是满足的if ( x > 0) ... else y = -x。如果 x < 0，则 y = -x 所以 y >= 0 满足，除非 -x < 0。所以前提是 { x >= 0 || -x >= 0 }。（唯一不正确的 x 值是最大负值，它会溢出。）

{ y >= 0 && |y| == |x| } 比 { y >= 0 } 更好，因为后者适用于所有类型的函数，而不仅仅是找到 x 的绝对值的函数（这可能是这段代码的用途，尽管您似乎省略了问题陈述）。

于 2013-02-28T05:15:48.463 回答
0

根据 和 的类型，这个问题的答案可能会变得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

于 2013-02-28T04:56:48.477 回答