Schleifeninvariante finden < Java < Programmiersprachen < Praxis < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 18:44 Fr 03.02.2012 | | Autor: | dennis2 |
| Aufgabe | Beweisen Sie, dass das folgende Code-Fragment den Durchschnittswert (a[0]+...+a[n-1])/n
berechnet, wenn die while-Schleife nach n Eingaben terminiert.
| 1: | ArrayList<Float> a = new ArrayList<Float >( ) ;
| | 2: | {
| | 3: | float x ;
| | 4: | float avg ;
| | 5: | int n ;
| | 6: |
| | 7: | avg = 0 ;
| | 8: | n = 0 ;
| | 9: | x = input ( ) ;
| | 10: | while ( x >= 0 ) {
| | 11: | avg = ( ( avg*n) + x ) / (n+1);
| | 12: | n = n + 1 ;
| | 13: | a . add ( x ) ;
| | 14: | x = input ( ) ;
| | 15: | } |
Zeile 16 lautet noch: @post: [mm] $\operatorname{avg}=\frac{\sum_{i=0}^{n-1}a.get(i)}{n}$
[/mm]
Definieren Sie dazu eine Schleifeninvariante, aus der bei Terminierung direkt die Nachbedingung
(s. Zeile 16) folgt. Beachten Sie, dass hier die Terminierung der Schleife nicht bewiesen werden
muss.
Verwenden Sie folgende Regel fur die add(...)-Funktion bei ArrayList:
| 1: | // s0
| | 2: | a.add(x);
| | 3: | // s1 = s0 + { a.get(s0(a.size())) -> s0(x), a.size() -> s0(a.size())+1 } |
|
Hallo!
Ich weiß, daß eine Schleifeninvariante vor Ausführung der Schleife, nach jedem Schleifenschritt und nach Beenden der Schleife gelten muss.
Ich komme jedoch auf keine Schleifeninvariante.
Hat jemand einen Tipp bzw. einen Ansatz für mich?
Beste Grüße
Dennis
|
|
| |
|
| Status: |
(Frage) überfällig | | Datum: | 14:40 Sa 04.02.2012 | | Autor: | dennis2 |
Wäre eine mögliche Schleifeninvariante:
[mm] $(n>0\Rightarrow avg=\frac{1}{n}\sum_{i=0}^{n-1}a.get(i))\wedge (n=0\Rightarrow avg=0)\wedge (n=a.size())\wedge (n\geq [/mm] 0)$
?
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 15:20 Mo 06.02.2012 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 19:20 Do 09.02.2012 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
