Verifikation/ Invariante

[babuschka]

Hallo!

Folgender Code ist gegeben und man soll beweisen, daß er den Mittelwert

(a[0]+.....+a[n-1])/n

berechnet, wobei davon ausgegangen wird, daß die while-Schleife nach n Durchgängen endet (was hier nicht bewiesen werden soll). Und zwar soll man das mittels einer Schleifeninvariante machen.

ArrayList<Float> a = new ArrayList<Float >( ) ;
{
float x ;
float avg ;
int n ;

avg = 0 ;
n = 0 ;
x = input ( ) ;
while ( x >= 0 ) {
avg = ( ( avgn) + x ) / (n+1);
n = n + 1 ;
a.add ( x ) ;
x = input ( ) ;
}
@post : n > 0 : \frac{1}{n}(\sum_{i=1}^{n-1}a.get(i))

In Zeile 16 soll das das arithmetische Mittel der Array-Einträge sein, ich wusste nicht, wie man hier LaTeX schreiben kann.

Dabei soll man benutzen:

// s0
a.add(x);
// s1 = s0 + { a.get(s0(a.size())) -> s0(x), a.size() -> s0(a.size())+1 }

Meine Fragen sind zunächst folgende.

1.) Verstehe ich das richtig, daß man zuerst eine leere ArrayList erzeugt und daß nach und nach mittels der (angedeuteten) input()-Methode Float Zahlen eingefügt werden?

2.) Wie könnte man auf die Schleifeninvariante kommen? Habe das noch nie gemacht. Ich weiß zwar grob, was so eine Schleifeninvariante erfüllen muss, aber nicht, wie man eine finden kann - nur, daß man immer recht kreativ sein muss und es keine allgemeine Regel dafür gibt.


Edit:

Kann man bei der Invarianten auch eine Oder - Konstruktion angeben?

 

[HimBromBeere]

...ich wusste nicht, wie man hier LaTeX schreiben kann.

Gar nicht, da hier nur statisches HTML angezeigt kann, oder einfacher: mach ein Bild draus und steck es in img-Tags.

Zu deiner ersten Frage:

ArrayList<Float> a = new ArrayList<Float>();

Damit legts du tatsächlich eine neue (leere) Liste an, aber befüllt wird sie mit

a.add(float)

Was das input() da soll, weiß ich nicht, ich schätze mal, da macht der Nutzer eine einmalige Eingabe, d.h. du musst das eigtl. IN die Schleife integrieren...
Der Rest sollte eigtl. so gehen, ist doch schließlich schon eine Schleifenvariante

 

[babuschka]

Wie meinst du das, daß es schon eine Schleifeninvariante ist?

 

[HimBromBeere]

Na, was ist denn das hier:

while ( x >= 0 ) {
	avg = ( ( avgn) + x ) / (n+1);
	n = n + 1 ;
	a.add ( x ) ;
	x = input ( ) ;
}

?

... was auch immer avgn darstellt (und v.a. wie du dieses Zeichen überhaupt geschrieben hast...)

 

[babuschka]

Es soll natürlich immer avg (=average) bedeuten, sorry-

Die Zeilen, die Du zitiert hast, sind die Schleife.


Aber was wäre eine Schleifeninvariante - - oder mißverstehe ich Dich?

 

[codechaos]

avgn soll wahrscheinlich avg*n bedeuten, weil das Ding sonst nicht den Durchschnitt berechnet.

Eine Schleifeninvariante ist eine Aussage, die in/nach jedem Durchlauf der Schleife stimmt. Zum Beispiel "Nach i Durchläufen der Schleife gift: n = i" oder "Nach i Durchläufen der Schleife enthält die Liste a die ersten i Eingaben".
Du musst nun eine geeignete Invariante finden, die dir etwas über den Durchschnitt aussagt. Damit kannst du dann einen Induktionsbeweis dafür führen, dass deine Schleife das richtige Ergebnis berechnet.

 

[babuschka]

Es ist mir klar, daß ich so eine Invariante finden muß.

Ich weiß aber nicht, wie man das hier macht. Daher habe ich ja meine Frage gestellt.

 

[codechaos]

Schau mal, wie die Variablen nach der Abarbeitung der Schleife belegt sind. Dann musst du schauen, ob sich daraus eventuell eine Aussage über einzelne Durchläufe ableiten lässt.
Du könntest auch ein paar Durchläufe per Hand durchspielen und schauen, ob dir da etwas auffällt, das dich dem Ziel deines Beweises näher bringt

 

[babuschka]

Leider bin ich immer noch nicht auf eine mögliche Schleifeninvariante gekommen.

Ich habe mir zwar mittlerweile zahlreiche Beispiele angesehen, aber ich komme hier partout auf keine.


Kann ich noch einen Tipp haben, falls man noch einen geben kann?


Grüße

 

[babuschka]

Okay, wahrscheinlich hat keiner mehr Lust, einen Tipp zu geben.

 

[babuschka]

Wäre eine mögliche Schleifeninvariante:

(n>0 --> avg=\frac{1}{n}\sum_{i=0}^{n-1}a.get(i)) und (n=0 --> avg=0) und (n=a.size()) und (n>=0)


??


Also ohne LaTeX kann ich das hier echt nicht schöner darstellen.

Also die "und" hätte ich sonst als \wedge dargestellt.