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
page revision: 1, last edited: 01 Feb 2018 14:11