Help finding a loop invariant.

Can someone help me find a loop invariant. The problem is,

x = a, y = b, s = 0
where A and B > 0.

while x =/= 0 do(
while x is even do (y= 2*y, x = x/2),
s = s+y, x=x-1)

when this loop finishes s = a*b

I need to find a loop invariant that is semantically equivalent to s=a*b

So when the loop starts it says s=0 and when the loop finishes it says s=a*b

s=ab-xy

looks like youre trying to multiply like a russian peasant.

>>3
Easy.