CODEWITHSUNDEEP
loop-invariant
carlos
carlos

Reputation: 5

Loop invariant for this code?

I've read about loop invariants, but I'm a little confused.
Let's say I have this code, what would the invariant be? Something like 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));
    }

Upvotes: 0

Views: 92

Answers (2)

mathfac
mathfac

Reputation: 196

The invariant is a condition that is always true in some part of code. The Loop invariant is a condition that is true inside the loop. Invariants are used to prove correctness of the program. The more useful invariant is for correctness proof more strong it is. I notated your program with strong invariants that show what program will recieve in 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
}

After that you can compare it with your program specification and make a decision if it works well even without running the code.

I used formula for arithmetic progression: formula. In the end of the loop I simply put last value of i in loop invariant and recieve invariant in the end of the program.

Hope I answered your question.

Upvotes: 1

tohava
tohava

Reputation: 5412

Reading the definition in wikipedia, I would guess the following:

A <= i <= B
resultado >= 0

Upvotes: 0

Related Questions