3 ms·
You can view it as induction, although the general case is slightly different. In the general case you have a while loop with some condition and invariant, and
by contravariant 11y ago
You can view it as induction, although the general case is slightly different. In the general case you have a while loop with some condition and invariant, and after the while loop stops your invariant is true and the condition is false, if you've done things correctly this then implies your 'goal'.
So to find a minimum in a list A[1],A[2],...,A[n] you can something like:
i := 1;
// Invariant: A[min] is the smallest in {A[1], ..., A[i]}
while not i = n do begin
if A[i+1] < A[min] then min:= i+1;
i:= i+1;
end
The negation of the condition: 'i = n', combined with the invariant: 'A[min] is the minimum of {A[1], ..., A[i]}', gives you the result you wanted.