Some people have expressed concerns about what the verify_table function does. Let me assure you that it does work. If your answer to Part I is right, then you should have no trouble figuring out it does.
Nevertheless, it may be difficult for you to come up with correct specifications for the function as it is now. So, I have slightly re-written the function. The main loop of the new function determines if the table is valid, unlike before. If so, it sets the boolean variable 'valid' to true, otherwise, it sets it to false. The small loop after the main loop isn't needed anymore.
Your task is still to give specifications for the main loop, and to prove that it's correct (which essentially proves that the function is correct).
Please use the new function.