Hallo!
Folgender Code ist gegeben und man soll beweisen, daß er den Mittelwert
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.
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:
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?
Folgender Code ist gegeben und man soll beweisen, daß er den Mittelwert
Code:
(a[0]+.....+a[n-1])/n
Java:
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))
Dabei soll man benutzen:
Java:
// 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?
Zuletzt bearbeitet von einem Moderator: