Korrektheit einer Schleife
{ V } while (B) do C { N }
beweist man durch geeignete Invariante I:
{ I und B } C { I }
