这不是我的作业——我只是在练习。我似乎无法完全理解这个断言概念。
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}.
最佳答案
如果你这样做是为了学习编程,你可以做一些编程来帮助你确认答案:
#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 的补码整数,其大小总是在之后匹配 - 它是标记极端情况的后置条件的符号部分。但是,对预期的内容有额外的了解仍然令人放心。
关于C++ 前提条件/断言,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15127451/