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