OOPM1718 Übungswoche 10 (29.01-04.02.18)

Zielsetzung für die Übung

  • Wiederholung zu allen Themen
  • Insbesondere
    • Algebraische Spezifikation
    • Verifikation von Algorithmen
Gegeben ist folgender Abschnitt einer Algebraischen Spezifikation für einen Mediaplayer:

sort Player

function start : Player -> Player

predicate istAn : Player
predicate istAmAbspielen : Player

Der Player kann nur gestartet werden, 
wenn er noch nichts abspielt, aber bereits an ist. 
Nach dem Starten ist der Player immer noch an 
und spielt das Medium ab. 
Definieren Sie eine Eigenschaft für die Funktion start.

property startEigenschaft(p) : Player.
    istAn(p) /\ ~istAmAbspielen(p) =>
        let p1 = start(p) in
            istAn(p1) /\ istAmAbspielen(p1)
Gegeben ist folgende Methode:

    public static int foo(int n) {
        {n>=0}
        int result = 3;
        int i = 1;
        while(i<n) {
            i++;
            result-=2;
            result *= i;
            result+=2;
        }
        return result;
        {result = n! + 2}
    }

Beweisen Sie mithilfe der Hoar'schen Regeln, 
dass für die gegebene Vor- und Nachbedingung 
der Algorithmus korrekt ist.
    public static int foo(int n) {
        {n>=0} => {n>=1} ?

        {n>=1}
        {1 <= n}
        {3 = 3 && 1 <= n}
        int result = 3;
        {result = 3 && 1 <= n}
        {result = 1! + 2 && 1 <= n}
        int i = 1;
        {result = i! + 2 && i <= n}
        while(i<n) {
            {result = i! + 2 && i <= n && i < n}
            {result = i! + 2 && i < n} =>

            {result = i! + 2 && i < n}
            {result = (i+1-1)! + 2 && i+1 <= n}
            i++;
            {result = (i-1)! + 2 && i <= n}
            {result - 2 = (i-1)! && i <= n}
            result=result - 2;
            {result = (i-1)! && i <= n}
            {result * i = i! && i <= n}
            result *= i;
            {result = i! && i <= n}
            {result + 2 = i! + 2 && i <= n}
            result+=2;
            {result = i! + 2 && i <= n}
        }
        {result = i! + 2 && i <= n && i >= n}
        {result = i! + 2 && i == n}
        {result = n! + 2}
        return result;

Der Algorithmus ist für die gegebene Vorbedingung nicht korrekt, 
da die gegebene Bedingung {n>=0} schwächer 
als die berechnete Bedingung {n>=1} ist.

Zielsetzung für das Programmierpraktikum

  • Wiederholung