Formale Verifikation - Aufgaben

Aufgabe:  

Folgendes Programm X berechnet aⁿ mithilfe von Quadrieren und Multi­plizieren:

p=a;
k=n;
y=1;
while (k>0)
{
    if (k%2==0)
    {
        p=p*p;
        k=k/2;
    }
    else
    {
        y=y*p;
        k=k-1;
    }
}

Zu zeigen ist die Korrektheit { Q } X { R } mit der Nach­bedingung R:  y = aⁿ. Wie lautet die schwächste Vorbedingung Q?