Oopm1516 Ex08
Zielsetzung für die Übung
- Hoare-Kalkül
{n >= 0}
i = 0;
k = -1;
y = 0;
while (i < n) {
i++;
k += 2;
y += k;
}
{y == n * n}
--------------------------------
n: 5 5 5 5 5 5
i: 0 1 2 3 4 5
k: -1 1 3 5 7 9
y: 0 1 4 9 16 25
Beziehung zwischen n und i:
0 <= i <= n
Beziehung zwischen y und i:
y = i*i
Beziehung zwischen k und i:
k = i * 2 - 1
{n >= 0
≡ 0 <= n
≡ 0 <= 0 <= n && 0 = 0*0 && -1 = 0 * 2 - 1}
i = 0;
{0 <= i <= n && 0 = i*i && -1 = i * 2 - 1}
k = -1;
{0 <= i <= n && 0 = i*i && k = i * 2 - 1}
y = 0;
I: {0 <= i <= n && y = i*i && k = i * 2 - 1}
while (i < n) {
I && B: {0 <= i <= n && y = i*i && k = i * 2 - 1 && i < n
≡ 0 <= i <= n && y = i*i && k = i * 2 - 1 && i + 1 <= n
≡ 0 <= (i + 1) <= n && y = i*i && k = i * 2 - 1 && i + 1 <= n
≡ 0 <= (i + 1) <= n && y + k + 2 = i*i + i * 2 - 1 + 2 && k + 2 = i * 2 - 1 + 2 && i + 1 <= n
≡ 0 <= (i + 1) <= n && y + k + 2 = (i + 1)*(i + 1) && k + 2 = (i + 1) * 2 - 1}
i++;
{0 <= i <= n && y + k + 2 = i*i && k + 2 = i * 2 - 1}
k += 2;
{0 <= i <= n && y + k = i*i && k = i * 2 - 1}
y += k;
{0 <= i <= n && y = i*i && k = i * 2 - 1}
}
I && !B: {0 <= i <= n && y = i*i && k = i * 2 - 1 && i >= n
≡ 0 <= i = n && y = i*i && k = i * 2 - 1
≡ 0 <= n = n && y = n*n && k = n * 2 - 1
≡ y = n * n}
Zielsetzung für das Programmierpraktikum
- Implementation von JUnit Tests (Blackbox-Test: Normalfälle, Grenzfälle, Fehlerfälle)
- Implementationen von Vor- und Nachbedingungen im Code
page revision: 2, last edited: 12 Jan 2016 10:38