{n >= 0}
    {true}
    {0 == 0}
    {0 == (1 - 1) * 1 / 2}
    i = 1;
    {0 == (i - 1) * i / 2}
    s = 0;
    {s == (i - 1) * i / 2}
    while (i <= n) {
        {s == (i - 1) * i / 2 && i <= n}
        [1]
        {s + i == i * (i + 1) / 2}
        s = s + i;
        {s == i * (i + 1) / 2}
        {s == (i + 1 - 1) * (i + 1) / 2}
        i = i + 1;
        {s == (i - 1) * i / 2}
    }
    {s == (i - 1) * i / 2 && n == i - 1 }
    {s == (i - 1) * (i - 1 + 1) / 2 && n == i - 1 }
    {s == n * (n + 1) / 2 && n == i - 1 }
    {s == n * (n + 1) / 2 && i == n + 1}
{s == n * (n + 1) / 2} => {I && !B}

Beweis zu [1]
{s + i == i * (i + 1) / 2}
{s == (i * (i + 1) - 2*i) / 2}
{s == (i^2 + i - 2*i) / 2}
{s == (i^2 - i) / 2}
{s == i*(i - 1) / 2}