Ex6 Partial/Total Correctness

uhweh
Neuling
Neuling
Beiträge: 10
Registriert: 16. Okt 2013 13:51

Ex6 Partial/Total Correctness

Beitrag von uhweh »

Hi,

in der 6.Übung Problem 4 und 5 wir gesagt, dass die Loop Invarianten partial correctness zeigen und in der c) wird jeweils gefragt, ob total correctness möglich ist.
Könnte mir bitte jemand erklären, was hier jeweils gemeint ist? Ich dachte die Begriffe hätten etwas damit zu tun, ob die Methode jweils terminiert oder nicht.
Aber damit komme ich hier nicht weiter.

Vielen Dank

tbjoe
Erstie
Erstie
Beiträge: 17
Registriert: 17. Okt 2013 10:27

Re: Ex6 Partial/Total Correctness

Beitrag von tbjoe »

Partial Correctness bedeutet, dass man zeigt, dass die Schleife korrekt ist, aber keine Aussage darüber macht, ob die Schleife terminiert.
Also man zeigt: Wenn es terminiert, ist es korrekt.

Total Correcctness heißt, dass man zeigt, dass die Schleife korrekt ist, also das berechnet, was man will, und auch terminiert.
Das wird durch die Symbole [p] und <p> in der dynamischen Logik ausgedrückt (p ist ein Programm).

Totale Korrektheit kann man nur beweisen, wenn man einen Term angeben kann, der mit jedem Schleifendurchlauf kleiner wird. Dafür benutzt man ein "decreases" Statement und "diverges true" muss man wegmachen.

Ich hoffe ich habe alles richtig wiedergegeben, für genauere Informationen, siehe Vorlesung 15 (vor allem ab Folie 19 ff) :)

uhweh
Neuling
Neuling
Beiträge: 10
Registriert: 16. Okt 2013 13:51

Re: Ex6 Partial/Total Correctness

Beitrag von uhweh »

Danke für die Erklärung.

Also könnte man bei Problem 4,5 c) sagen, dass es möglich ist Total Correctness zu zeigen, da decreasing terms existieren?

Antworten

Zurück zu „Archiv“