Aufgabe 10:  (Bitlänge einer natürlichen Zahl a berechnen)

Sie berechnen die Bitlänge einer natürlichen Zahl a, indem Sie die kleinste Zweierpotenz 2^k bestimmen, die größer als a ist. Für a = 13 beispiels­weise ist 2⁴ = 16 diese kleinste Zweierpotenz. Der Exponent k = 4 entspricht genau der Bitlänge von a.

Gegeben sei folgendes Programm X:

Das Programm X berechnet den kleinsten Exponenten k, derart dass 2^k > a gilt.

Ermitteln Sie die schwächste Vorbedingung Q für die Korrektheits­formel {Q} X {R} mit der Nach­bedingung

R:   2^k > a

Wenn das Programm terminiert, dann ist k der kleinste Exponent, der diese Nach­bedingung erfüllt, da k bei 0 beginnt und bei jedem Schleifen­durchlauf um 1 größer wird.

Hinweis: Gehen Sie schrittweise vor. Beweisen Sie zunächst die While-Schleife, indem Sie die beiden Prämissen der Schlussregel für die While-Schleife beweisen. Ermitteln Sie aus der ersten Prämisse die Schleifen­invariante P. Bringen Sie die Nach­bedingung R in die Form P ∧ ¬B, indem Sie die Variable p in die Nach­bedingung hinein­bringen.

Aufgabe 11:  Beweisen Sie die totale Korrektheit des Programms zur Berechnung des Rests bei ganzzahliger Division aus der vorigen Aufgaben­serie.

Hinweis: Für den Beweis der totalen Korrektheit müssen Sie die Schleifen­invariante P verschärfen, damit es einen ganzzahligen Ausdruck E gibt, der im Schleifen­körper vermindert wird und für den E > 0 aus P ∧ B abgeleitet werden kann.