Invarianten finden?

Für gegebene Schleifen sind Invarianten schwer zu finden.

Deswegen (,,Extreme Programming`` a la Hoare, Dijkstra):

Oft sind Invarianten durch Datenstrukturen vorgegeben (Baum soll heap-geordnet oder balanciert oder Suchbaum sein)

Beispiel Heap-sort. Struktur-Invariante ist:

$ \forall$1 < k < n : a[$ \lfloor$k/2$ \rfloor$]$ \ge$a[k]



Johannes Waldmann 2006-06-26