ExponenciacionEficiente.gcl

[Ctx C: a, b: nat & b>=0
    {Q: T}

    x, y, z := a, b, 1;

    {Inv P: y>=0 & z*x^y = a^b}

    {cota t: y}

    do y > 1 ->
        if y mod 2 = 0 ->
            x, y := x * x, y / 2;
        [] y mod 2 != 0 ->
            z, x, y := z * x, x * x, (y - 1) / 2;
        fi
    od

    z = x * y;

    {R: z = a^b}
]