Prove that this program (in simple programming language) never reports error:

N = 20;
i = N;
x = 2;
while (i > 0) {
  x = x + 4;
  i = i - 1;
}
if (x==0) {
  error; // assert(false)
} else {
  y = 1000/x;
}

Solutions we know so far:

• execute program (what if N=2000000)? What if N is not known?
• symbolically execute program (how many times will we go through loop?)
• provide sufficient loop invariant
  • what is loop invariant suficient to prove x!=0 after loop?
  • today: steps towards computing it