How to proof that the predicates before and after the loop holds

81 Views Asked by At

So this is the loop: predicate

$ m + n = odd$

$while (m>=0 $ and $m <=100)$

$m = m +4$

$n = n -2$

$end while$

So this loop is supposed to be true before and after the loop, but i dont know why. Before the loop we have:

$m +n $ = $m+4 +n -2$

if we then have m = 0, because thats the start we get an even number. So how is m +n supposed to be odd before and after the loop