int i = 0
boolean answer = false
while (i < a.length) {
if a[i] == 0
answer = true
i = i + 1
where 'a' is an array of integers. I'm doing a question paper where it has asked me what the loop invariant of this is, I have already established that the code works out whether the array contains a 0. But so far I can only think of the invariant as being
i <= a.length
and the question states to include variables i, a and answer in the invariant so I know this can't be right. I have not come across loop invariants involving booleans before and am confused, could anyone help explaining?
Here is an implementation of your loop in Microsoft Dafny with appropriate loop invariants specified:
You can verify its correctness automatically in the online version of Dafny