Consider the following piece of code segment. begin x := a ; y := b; s := 0 ; while x <> 0 do begin while not ( odd (x) ) do begin y := 2 * y ; x := x div 2 ; end; s := s + y ; x := x 1 ; end; end.

The above code is intended to compute the product a * b and leave the result in s. Assume that a and b are non-negative integers. Trace the code three for different a, b pairs. A more challenging but do-able task: How can we formally argue that the code is indeed correct.