2

加速されたc++を読んでいるときに、不変条件がfalseになる理由についての説明に混乱しました（以下のコードを参照）。

不変条件は、作成者（この場合）によって次のように定義されています。

whileの不変条件は、これまでにr行の出力を書き込んだことです。rを定義するときは、初期値0を指定します。この時点では、何も記述していません。rを0に設定すると、明らかに不変条件が真になるため、最初の要件を満たしています。

// invariant: we have written r rows so far
int r = 0;

// setting r to 0 makes the invariant true
while (r != rows) {
    // we can assume that the invariant is true here

    // writing a row of output makes the invariant false <- WHY?
    std::cout << std::endl;

    // incrementing r makes the invariant true again
    ++r;
}   
// we can conclude that the invariant is true here

その後、説明します...

出力の行を書き込むと、rが書き込んだ行の数ではなくなるため、不変条件がfalseになります。

定義を考えると、私は2つの間の接続を形成することはできません。

出力の行が書き込んでいるときに不変条件がfalseになるのはなぜですか？

4

2 に答える 2

3

r印刷された行数として定義されます。したがって、不変式は次の場合にのみ真になります。

r == number of rows that have been printed

r行を印刷してから、これまでに印刷された行数を更新するためにインクリメントするまでの間、その不変条件は当てはまりません。

rはある数値 (たとえば ) に等しくn、「印刷された行の数」はその数値 ( n + 1) よりも 1 大きくなります。これは、印刷したばかりの行のためです。したがって、不変式は真ではありませんn != n + 1。

于 2012-06-01T22:52:19.040 に答える
0

これまでに r 行の出力を書きました

rcoutは 0 から始まり、 r が 0である点ではまだ 0 です。coutは 1 行書きましたrが 0 です。したがって、不変式は一時的に偽ですr。これまでに 0 行の出力を書き出しました。」

インクリメントrすると、不変条件が再び真になります。

于 2012-06-01T22:52:28.007 に答える