Terminierung while-Schleife < Algor.+Datenstr. < Theoretische Inform. < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) überfällig  | | Datum: | 19:20 Mi 10.05.2006 | | Autor: | dump_0 |
Hi.
Ich soll beweisen, dass folgendes "Programm" terminiert:
(*[tex]a = 0 \wedge n \ge 0[/tex]*) <-- Vorbedingung
WHILE [tex](a + 1)^2 \le n[/tex] DO
[tex]a := a + 1[/tex]
END
(*[tex]a^2 \le n < (a + 1)^2[/tex]*) <-- Nachbedingung
Ich habe leider noch nicht viel bzw. garnichts von Beweisen bzgl. Terminierung gehört, daher kann ich nicht viel damit anfangen. Wie man aber die partielle Korrektheit von Programmen mittels des Hoare-Kalküls zeigt ist kein Problem.
Ich hoffe ihr könnt mir helfen :)
mfg
[mm] dump_0
[/mm]
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 19:20 Fr 12.05.2006 | | Autor: | matux |
$MATUXTEXT(ueberfaellige_frage)
|
|
|
|
