0

ループ不変条件について読んだことがありますが、少し混乱しています。
このコードがあるとしましょう。不変条件は何でしょうか? A+B =X のようなもの？

    public static void main(String[] args) {
      Scanner scanner = new Scanner(System.in);
      long A = scanner.nextLong();
      long B = scanner.nextLong();

      long resultado = 0;

      for (long i = A; i <= B; i++) {
          resultado += Long.bitCount(i);
      }

      System.out.println(Long.valueOf(resultado));
    }
4

2 に答える 2

1

不変条件は、コードの一部で常に true である条件です。ループ不変条件は、ループ内で真となる条件です。不変条件は、プログラムの正しさを証明するために使用されます。より有用な不変式は、より強力な正当性の証明に使用されます。resultadoでどのプログラムが受け取るかを示す強​​力な不変条件を使用して、プログラムに注釈を付けました。

public static void main(String[] args) {
  Scanner scanner = new Scanner(System.in);
  long A = scanner.nextLong();
  long B = scanner.nextLong();

  long resultado = 0;

  for (long i = A; i <= B; i++) {
      resultado += Long.bitCount(i); 
// loop invariants: 
// strong: resultado = A + (A + 1) + ... + i => resultado = (A + i) * (i - A + 1) / 2,
// weak: resultado > A, A <= i <= B
  }

  System.out.println(Long.valueOf(resultado)); //invariants: resultado = (A + B) * (B - A + 1) / 2,  this invariant prooves correctness of the program
}

その後、プログラムの仕様と比較して、コードを実行しなくてもうまく機能するかどうかを判断できます。

等差の式を使用しました: 方式. ループの最後に、 iの最後の値をループ不変条件に入れ、プログラムの最後に不変条件を受け取ります。

あなたの質問に答えていただければ幸いです。

于 2014-08-01T10:11:15.737 に答える