OOPM1718 Übungswoche 07 (08.01-14.01.18)

Zielsetzung für die Übung

  • Verifikation von Algorithmen
    • Beweis von Zuweisungen
    • Beweis von Anweisungssequenzen
    • Beweis von While-Schleifen
    • Beweis von If-Anweisungen
  • Bestimmung von Schleifeninvarianten
  • Ausnahmen und deren Behandlung
    • Vorlesungsfolien ab Seite 40

Beispiel

{n >= 0} =>
        {n >= 0}
        int k = n;
        {x^k == x^n && k >= 0}
        int p = x;
        {p^k == x^n && k >= 0}
        int y = 1;
        {y * p^k == x^n && k >= 0}
        while (k > 0){
            I && B = {y * p^k == x^n && k > 0}
            if (k % 2 == 0) {
                {y * p^k == x^n && k >= 0}
                {y * (p*p)^(k/2) == x^n && k >= 0}
                p = p * p;
                {y * p^(k/2) == x^n && k >= 0}
                {y * p^(k/2) == x^n && k/2 >= 0}
                k = k / 2;
                {y * p^k == x^n && k >= 0}
            } else {
                {y * p^k == x^n && k > 0}
                y = y * p;
                {y * p^(k-1) == x^n && k > 0}
                {y * p^(k-1) == x^n && k-1 >= 0}
                k = k - 1;
                {y * p^k == x^n && k >= 0}
            }
        I = {y * p^k == x^n && k >= 0}
        }
        I && !B = {y * p^k == x^n && k == 0}
        {y == x^n && k == 0} =>
{y==x^n}

I = {y * p^k = x^n && k >= 0}

Wenn eine Bedingung P gegeben ist und eine andere Bedingung P' mithilfe der Hoar'schen Regeln berechnet wurde, dann muss P=>P' gelten (P muss stärker als P' sein).

Zielsetzung für das Programmierpraktikum

  • Ausnahmen
    • Kennenlernen von bekannten Exceptions (NullPointerException, …)
    • Erstellen von eigenen Exception
    • Werfen von Exception mit throw
    • Exception vs. Error
    • RuntimeException vs. Exception
  • Ausnahmebehandlung
    • try/catch-Blöcke