Gesucht ist die Länge n der Binärdarstellung einer natürlichen Zahl a. So hat beispielsweise die Zahl a = 13 die Binärdarstellung 1101, denn 13 = 1·8 + 1·4 + 0·2 + 1·1. Die Binärdarstellung der Zahl 13 beansprucht 4 Ziffern, die Bitlänge beträgt also 4.
Die Bitlänge einer natürlichen Zahl a lässt sich berechnen, indem die kleinste Zweierpotenz 2k bestimmt wird, die größer als a ist. Für a = 13 beispielsweise ist 24 = 16 diese kleinste Zweierpotenz. Der Exponent k = 4 entspricht genau der Bitlänge von a.
Aufgabe: (Berechnung der Bitlänge einer natürlichen Zahl a)
Gegeben sei folgendes Programm X:
Das Programm X berechnet den kleinsten Exponenten k, derart dass 2k > a.
Ermitteln Sie die schwächste Vorbedingung Q für die Korrektheitsformel {Q} X {R} mit der Nachbedingung
R: 2k > a
Wenn das Programm terminiert, dann ist k der kleinste Exponent, der diese Nachbedingung erfüllt, da k bei 0 beginnt und bei jedem Schleifendurchlauf um 1 größer wird.
Alternativ kann die Nachbedingung etwas komplizierter als 2k-1 ≤ a ∧ 2k > a gewählt werden.
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 Schleifeninvariante P.
Weiter mit: [up]