Benutzer-Werkzeuge

Webseiten-Werkzeuge


glossar:schleifeninvariante

Schleifeninvariante

engl.: loop invariant

Bedeutung

Sei W = while(b){S} eine Schleife mit seiteneffektfreier Bedingung b.

Eine Schleifeninvariante INV zur Schleife W ist ein boolescher

Ausdruck/eine logische Formel mit der Eigenschaft:

{ b && INV } S { INV }

Bemerkungen

  • Die zentrale Schwierigkeit bei der Verifikation von nicht-rekursiven prozeduralen Programmen ist das Entwickeln geeigneter Schleifeninvarianten.
  • Schleifeninvarianten sind auch ein hervorragendes Dokumentationsmittel, da sie die algorithmische Idee ausdrückt, die der Schleife zugrunde liegt.
glossar/schleifeninvariante.txt · Zuletzt geändert: 2016/09/22 10:14 (Externe Bearbeitung)