I am currently in an introductory programming class and was asked to interpret the final state of the given tracing table featuring a loop invariant. The blue numbers in the bottom box are the given answers.
As you can see, low is updated but I don't know how this number was achieved given the information in the contract.
Edit: Is a correct method to solving this finding the "boundary" values where the expressions in the @maintains clause hold true?
Since n doesn't change, high at the least can be 81, and low at the greatest is 9?
So this would be confusing if you didn't understand the full definition of the loop invariant, like I did.
A loop invariant is a conditional statement that is true at the beginning of the method, before and after each iteration, and at the end of the method. Otherwise, it is not a valid loop invariant.
Knowing variables low and high are updated, we know their values have a chance of being changed in the method. n, on the other hand, will remain the same.
The loop invariants are low * low <= high and low * low <= n <= high. These must hold true at the end of the method body.
The loop only runs when low * low < high, i.e., the loop stops once low * low >= high. But, low * low > high cannot happen due to our loop invariant (equals-to symbol omitted for clarity)!
So following the rule that the loop invariant must hold, and knowing when the while loop stops, it's concluded that the final values must be:
low * low = high.
Factor in n and we have low * low = n = high. Again, we know low and high are the only values that have a chance of being changed.
Finally, we have low * low = 81 = high.
low = 9, n = 81, high = 81.
