Algorithmen und Programmierung II

 SS 2004
Übungsblatt 12
 Abgabe: 8.7.2004


Aufgabe 1 (5 Punkte)

Gesucht ist eine formale Spezifikation für die Methode
    void rearrange(int low, int high)
in Anlehnung an das rearrange aus 2.3.2, Seite 5/6.  Voraussetzung und Effekt sollen in Haskell formuliert werden.


Aufgabe 2 (6 Punkte)

Beweisen Sie:
    final int a[] = new int[n];
    int mitte, unten, oben, x;  .....
   { a[unten]<x<a[oben] ∧ mitte=(unten+oben)/2 ∧ a[mitte]≠x ∧ ∀unten≤i<k≤oben a[i]<a[k] }
    if (a[mitte]<x) unten = mitte; 
    else            oben  = mitte;
  { a[unten]≤x≤a[oben] }
Lässt sich die Voraussetzung abschwächen?  Wenn ja, geben Sie eine geeignete schwächere Voraussetzung an!  Wenn nein, warum nicht?


Aufgabe 3 (9 Punkte)

Die folgende Methode berechnet das Produkt zweier natürlicher Zahlen mit der als „Ägyptische Multiplikation“ bekannten Technik:
    /** 
     * pre:  a>=b && b>=0
     * post: result == A*B
     */
    static int product(int a, int b) {
           int p = 0;
           while (b>0) {
                 if (b%2==1) p += a;
                 b = b>>1;
                 a = a<<1; }
           return p;
    }
a)  (8 P.)  Beweisen Sie die partielle Korrektheit unter Verwendung der Schleifeninvariante
    b>=0 && p+a*b == A*B
b)  (1 P.)  Beweisen Sie die totale Korrektheit!