El siguiente bucle while implementa una forma de multiplicar dos números que fue desarrollada por los antiguos egipcios. [Pre-condición: A y B son ...

El siguiente bucle while implementa una forma de multiplicar dos números que fue desarrollada por los antiguos egipcios. [Pre-condición: A y B son números enteros positivos, x A y B y producto 0.] while (y 0) r : y mod 2 if r 0 then do x : 2 x y : y div 2 end do if r 1 then do producto : producto x y : y ฀ 1 end do end while [Post-condición: producto A B] Demuestre la exactitud de este bucle con respecto a su pre y post-condiciones por medio del invariante del bucle I (n): “xy producto A B”.