# Hoare correctness proof for a recursive definition of multiplication

Given the program:

{y=y0 ^ y>=0}
z=0;
while (y>0){
z=z+x;        (1)
y=y-1;
}
{z=x*y0}


I am having trouble finding the invariant, I've tried:

• z=xy-xy
• z<=xy
• z=0xy

with/without the precondition as the invariant, but none of my attempts can be used to prove the post-condition. Any help would be greated appreciated!

Moreover, if the code at (1) is changed to z=z*x;, how should I modify my invariant?

• Try z = xy0 -xy – Dmitri Chubarov Nov 23 '17 at 7:37
• @Dmitry Make an answer? – Yuval Filmus Nov 24 '17 at 19:06