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

不变量是在代码的某些部分中始终为真的条件。循环不变量是循环内部为真的条件。不变量用于证明程序的正确性。更有用的不变量是为了更强大的正确性证明。我用强大的不变量标记了您的程序，这些变量显示了在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 回答
0

阅读维基百科中的定义，我猜如下：

A <= i <= B
resultado >= 0
于 2014-07-30T10:20:12.020 回答