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

xこれを実行すると、 -128（-128）で失敗するかどうかがわかりますy。これは、2の補数表記の非対称性によるものです。-128は8ビット文字で表すことができますが、128はできません（127のみ）。

したがって、1の場合、2の補数整数を想定すると、前提条件はx、ビット幅で表現可能な最小値ではないということです。もちろん、xとyがintでさえあるという質問には何もありませんので、それはすべて少し暫定的です。

xとが浮動小数点数または倍精度浮動小数点数である場合y、通常の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

x> 0の場合、y>=0は常に満たされif (x > 0) y = xます。x == 0の場合、y>=0は常に満たされif ( x > 0) ... else y = -xます。x <0の場合、y = -xであるため、-x <0でない限り、y> = 0が満たされます。したがって、前提条件は{x> =0||です。-x>=0}。（それが当てはまらないxの唯一の値は、オーバーフローする最大の負の値です。）

{y> = 0 && | y | == | x | }は{y>=0}よりも優れています。後者はxの絶対値を見つける関数だけでなく、あらゆる種類の関数に当てはまるからです（これはおそらくこのコードの目的ですが、問題の説明）。

于 2013-02-28T05:15:48.463 に答える
0

投稿条件から逆方向に作業します。分岐ステートメントは 1 つだけです。if ステートメントは x > 0 をテストするので、 、 、 の 3 つのケースx < 0をx == 0調べx > 0て、x のどの値が事後条件を満たしているかを判断します。

于 2013-02-28T04:28:54.617 に答える
0

これに対する答えは、 と のタイプによっては厄介になる可能性がxありyます。@PeteFordham が指摘したように、2 の補数の整数は対称的ではないため、負の最大整数の絶対値を表すことはできません。整数の代わりにxandyがfloatorの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 に答える