Korrektheitsbeweis < Algor.+Datenstr. < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 21:13 Do 15.04.2010 | | Autor: | DerGraf |
Hallo,
mir ist ein Sortieralgorithmus in folgender Form gegeben:
Vorbedingung: Array a der Länge n
Nachbedingung: für alle [mm] a_i [/mm] und [mm] a_j [/mm] mit 0 [mm] \le [/mm] i < j < n gilt [mm] a_i \le a_j
[/mm]
$ [mm] "\n" [/mm] $
k [mm] \leftarrow n/2 $ "\n" $
while k>0 do $ "\n" $
for 1=k,...,n-1 do $ "\n" $
e \leftarrow a[i] $ "\n" $
j \leftarrow i $ "\n" $
while(j \ge k && a[j-k] > e) do $ "\n" $
a[j] \leftarrow a[j-k] $ "\n" $
j \leftarrow j-k $ "\n" $
end while $ "\n" $
a[j] \leftarrow e $ "\n" $
end for $ "\n" $
k \leftarrow k/2 $ "\n" $
end while $ "\n" $
Zu diesem Algorithmus soll ich nun einen Korrektheitsbeweis führen. Dabei hatten wir in der Vorlesung Schleifeninvarianten benutzt, um die richtige Ausgabe nachzuweisen. Ich habe allerdings keine Ahnung , wie ich das hier machen soll. Kann mir da jemand etwas auf die Sprünge helfen?
Ich bin für jede Hilfe dankbar.
Gruß
DerGraf
[/mm]
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 18:20 Fr 16.04.2010 | | Autor: | DerGraf |
Ich habe mich nochmal intensiv mit der Aufgabe befasst und würde die Invariante für die mittlere Schleife wie folgt formulieren:
a[i]>a[i-k]>...>a[i-x*k] mit x [mm] \in \IN [/mm] und [mm] i-x*k\ge0 [/mm]
|
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig | | Datum: | 21:20 Mo 19.04.2010 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
