Das siehst du richtig. Ist auch gar nicht immer (nie?) einfach ihn zu bestimmen, aber da es keinen Algorithmus zum automatischen Bestimmen gibt, ich dir also kaum mehr als in der Wikipedia steht, erzählen kann, würde ich sagen: Poste mal deinen Code und wir versuchen zusammen unser Glück.

Eine Schleifeninvariante ist die Beziehung zwischen den in einem Programm vorkommenden größten Werte, die vor Eintritt in die Schleife gelten, sowie während der Ausführung unverändert (invariant) bleiben.

Die Schleifeninvarianten sind das Herzstück des Hoare-Kalküls.

Zu überlegen, was sich in einer Schleife nicht ändert, ist zunächst ungewohnt, liefert aber meist interessante Einsichten in die zugrundeliegende algorithmische Idee.

Auffinden geeigneter Invarianten ist anspruchsvoll und zurzeit nicht komplett automatisierbar.

Eine Invatriante für i = x wäre z.B. 0 <= x <= i.
In Worten: x ist endweder gleich dem Startwert oder kleiner (aber nicht negativ).

Es kommt ja darauf an, was du damit vorhast, um die Korrektheit deines Programmes zu beweisen. Oft ist ein einfacher Algorithmus für das Problem besser geeignet, da die Invariate sonst recht schwer zu finden ist.

Aber ich sage aus Erfahrung:
Viel Spaß! :mrgreen:

Reche das doch einfach mal durch.

DIE Invariante gibt es nicht, es gibt einfach welche, mit denen man zum Ergebnis kommt und welche, mit denen man das nicht schafft.

Aber eine Gleichheitsaussage über a zu treffen geht vielleicht nicht, da a ja nicht gleich bleibt während eines Schleifendruchlaufes.
Was wollt ihr mit der Invarianten überhaupt machen?
Zur Not such in diesem Script einfach mal na Invariante, vielleicht hilft das ja weiter.
http://ls5-www.cs.uni-dortmund.de/ls5Medien/Dokumente/Lehre/DAP1/skript-dap1-ws0607.pdf

"Max123" schrieb:

Eine Invatriante für i = x wäre z.B. 0 <= x <= i.
In Worten: x ist endweder gleich dem Startwert oder kleiner (aber nicht negativ).

Nein, das stimmt nicht. Der Sinn von Invarianten ist es, Schleifen/Funktionen besser zu verstehen, mit dem Ziel beweisen zu können, das etwas funktioniert oder eine Schleife endet. Deswegen lässt man sich nicht davon verleiten zu gucken was ein Programm eigentlich machen soll (Quadrieren), sondern guckt auf das was sich ändert/was nicht und was vor der Schleife und was nach der Schleife gilt.

Ums auf den Punkt zu bringen: Wenn ich der Funktion -4 übergebe, wird 0 zurückgeliefert, x bleibt unverändert. Das ist nicht nur falsch, sondern die Invariante von Max123 stimmt nicht. Du wirst eine Fallunterscheidung brauchen, weil sich die Funktion nicht regelmäßig verhält.

Hmm, das Problem würde ein x = x<0 ? 0 : x; lösen.
Bin ich froh, dass ich meine Klausur darüber weg hab... xD

Dann würde deine Invariante stimmen, aber das Quadrieren wäre bei negativen Zahlen immernoch falsch. Sinnvoller wäre sowas x<0 ? x=-x;

Was mich interessieren würde (ist schon etwas her, seit dem ich das lernen musste):
Betrachtet man nur die Zählvareable der Schleife oder können alle Vareablen, von denen man innerhalb der Schleife zugreifen kann, betrachtet werden?
Werden auch Einschränkungen betrachtet, die außerhalb der Schleife für die Vareable festgelegt werden?
Ist x >= 1 und a >= 0 richtig?

Jede Schleife kennt die Variable, die drum herum steht. Du musst für eine Schleife keine extra Variable initialisieren.

Wenn du jetzt ne Variable innerhalb einer Schleife setzt, wird diese nach dem Schleifendurchlauf wieder freigebene. Aber prinzipiell kannst du auch andere Variablen aus deiner Funktion benutzen.

Man betrachtet sinnvollerweise nur Variablen die in der Schleife verändert werden oder Einfluss auf das Ergebnis haben.