invariante

[Ahnung]

was genau versteht man unter einer Invariante (im Bezug auf Schleifen) und wofür ist die Bestimmung nützlich ?

[mrdigital]

Eine Invariante ist das Selbe nur anders gesagt ;)

[Xmas]

Eine Schleifeninvariante ist eine Bedingung, die sowohl bei Schleifenbeginn als auch bei Schleifenende gilt (gelten muss). Dies kann man zur Verifikation verwenden.

[Trap]

Eine Invariante ist ein ja-nein-Aussage die bei jedem Schleifendurchlauf wahr bleibt. Oft ist das eine bessere Beschreibung dessen was die Schleife macht als eine Beschreibung was sich ändert.
z.B. bei Sortierverfahren die Aussage "die ersten $schleifenvariable Elemente sind sortiert". Was bei $schleifenvariable=Arraygröße automatisch die Aussage "das Array ist sortiert" ergibt.

Interessant ist auch die Schleife mit Hilfe einer Invariante zu konstruiren, das hilft bei komplexerene Schleifen sehr. Dazu hab ich auf meinem anderen Rechner eine klasse Anleitung, aber grad keine Zeit zum posten, mach ich später.

BTW: Es gibt auch Objekt-Invarianten, auch wichtig und eine gute Hilfe beim Entwerfen von Klassen.

[Crushinator]

Ich versuch's jetzt auch mal: Eine Invariante beschreibt was invariant, also unveränderlich ist. Bei Schleifen ist sie ein arithmetischer Ausdruck, der sich innerhalb derer nicht ändert bzw. immer gültig ist.

Ein ganz einfaches Beispiel:

int ExampleFunc(int n, int x)
{
int i = n;
int res = 1;

while (i > 0)
{
i--;
res = res*x;
}
return res;
}

Die Schleifeninvariante lautet hier: res = x ^ (n-i)

Ein etwas kompliziertes Beispiel, der zeigt daß am Ende der Schleife zwar die Schleifeninvariante noch gilt, aber auch gleichzeitig negiert zur Schleifenbedingung ist:

int ExampleFunc(int n, int x)
{
int i = n;
int res = 0;

while (i>0)
{
i--;
res=res+x;
}

return res;
}

Hier gilt INV = res + x * i. Der Ausdruck ändert sich innerhalb der Schleife nicht, und am Ende ist INV gleich mit i, also 0.

So, jetzt raucht auch mir der Kopf. :D

[Ahnung]

danke schön

[Trap]

Ich versuch's jetzt auch mal: Eine Invariante beschreibt was invariant, also unveränderlich ist. Bei Schleifen ist sie ein arithmetischer Ausdruck, der sich innerhalb derer nicht ändert bzw. immer gültig ist.

Wie kommst du auf arithmetischer Ausdruck? Eine Gleichung ist ein boolescher Ausdruck. Aber nur eine mögliche Form davon, genauso ist "die erste i Elemente sind sortiert" eine mögliche Invariante.

Es gibt auch noch eine Schleifenvariante (ohne in-), das ist ein arithmetischer Ausdruck mit dem man das Terminieren der Schleife kontrollieren/sicherstellen kann. Die Variante ist ein Ausdruck mit Wert >0 der bei jedem Durchlauf kleiner wird. Bei For-Schleifen ist das trivial, bei manchen do-while oder while-Schleifen ist das ganz hilfreich.

[Crushinator]

Ja, nenn' es von mir aus einen boolschen Ausdruck. Mit arithmetischem Ausdruck versuchte ich nur zu erklären, daß es sich um eine Formel handeln kann. :)

[Trap]

So, hier noch die versprochene Anleitung:
Floyd and Hoare developed the method of proving, by induction, that a given
program containing a loop implements a given specification. The Gries method
inverts this by guessing parts of the induction proof, and using the
specification and supposed proof to construct the program:

1. Write a specification for the code in unambiguous language (or formal
notation).
2. Identify all trivial cases and write the programs that solve them. This
is the loop postlogue
3. Identify the qualities that distinguish the trivial cases from all
other inputs. Write code to check for these qualities. This is the loop
condition.
4. Identify a measurement on the inputs that is bounded below by zero for
all possible inputs and is zero for the trivial cases. Make a new copy
of the specification that includes this measurement as a variable.
5. Further modify the copy so that the measurement can be anywhere between
its original and minimum values. Determine the difference between the
output of the original case and the output of any intermediate case.
Require the output variables (in the spec copy) to have values
that summarize this difference. If there aren't enough output
variables to do this, create them. This spec is the loop invariant, and
can be made into test code if desired.
6. Write code that assigns the output variables values that make the
invariant true for the initial value of the measurement. This is the
loop initialization.
7. Choose a way of reducing the measurement (e.g. decrementing, halving).
8. Substitute the expression for the reduced measurement into the invariant
to determine how each variable needs to change, when the measurement is
reduced, to make the invariant true again. Write code to make these
changes. This is the loop body.

If you complete all of these steps, you will have a program that is correct
by construction. The main judgement calls are what constitutes a trivial
case, what measurement to use, how to reduce it. Furthermore, "write code"
might involve a recursive application of the method.

[Aqualon]

Hab auch eine Frage zur Schleifeninvariante. Nehmen wir mal folgenden Code zur Generierung der n-ten Fibonacci-Zahl.


int fib(int n) {
int a,b,i;

a=0; b=1; i=0;

while(i<n) {
i=i+1;
b=a+b;
a=b-a;
}

return a;
}
Gibt es bei dieser while-Schleife eine Invariante? Ich wuesste nicht, wie man nach jedem Schleifendurchlauf aus a, b und i auf die n-te Fibonacci-Zahl kommen koennte. Ich seh noch, dass a immer die i-te Fibonacci-Zahl ist und b die (i+1)-te Fibonacci-Zahl, aber kann man daraus schon auf eine Invariante schliessen?

Aqua

[Trap]

Eine Invariante gibt es sicher: b>=a
Die ist aber nicht streng genug, dass daraus folgt, dass man Fibonaccizahlen erzeut.

Eigentlich hast du deine Invariante ja schon genannt: fib(i)==a && fib(i+1)==b
Je nachdem für welchen Zweck du die Invariante benutzt kann das schon die sinnvollste Invariante sein.