Wrong Invariants

Regarding the topic, I’m trying to understand why my implementation fails the test Prog2.tests.daily.VerificationTests::testWhileWrongInv. All cases that I considered and tested so far seems to work with my implementation (my code pass them).

A loop invariant is wrong, if:

  • it doesn’t hold for the loop body regardless of the rest program
  • it is too weak such that it cause the assertion condition not to work.
  • it belongs to an inner loop and the outer loop’s bound k is shadowed by a local variable in the outer loop body
  • it belongs to an inner loop and doesn’t contain the outer loop’s condition (i.e the invariant of the outer and inner are identical).

I’ve tested the cases, where the invariant is valid, as well. The implementation passes all tests.
All tests are pushed to the server.

I will be grateful for any hint about this issue to pass this daily test.

Looking at your code, you did not implement what I told you yesterday…