Enter your search text in the box above

Select a result to preview

Terminierungsfunktion

#Studium #Informatik #Definition #SWTPP

Für den Beweis der totalen Korrektheit einer Schleife benötigt man eine Funktion t:State→N (Schleifenvariante), für die gilt:

  1. I∧b⇒t≥0 (Beschränktheit nach unten).
  2. {I∧b∧t=m} S {I∧t<m} (Strikter Abstieg in jedem Durchlauf).