Benutzer-Werkzeuge

Webseiten-Werkzeuge


glossar:schleifeninvariante

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen gezeigt.

Link zu dieser Vergleichsansicht

glossar:schleifeninvariante [2017/09/26 10:20] (aktuell)
Zeile 1: Zeile 1:
 +====== 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: 2017/09/26 10:20 (Externe Bearbeitung)