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: 24.09.2014 16:47 (Externe Bearbeitung)
 
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki