Exercise 6 - Partial Correctness vs. total correctness

barracuda317
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

Exercise 6 - Partial Correctness vs. total correctness

Beitrag von barracuda317 »

Hallo,

leider bin ich noch unsicher was Partial Correctness und total correctness angeht?

Bisher habe ich die Begriffe wie folgt verstanden:

Partial correctness: Es ist nicht sichergestellt, dass das Programm terminiert, aber wenn es terminiert, dann gilt auch die Formel.

Total correctness: Das Programm terminiert immer, und nach der Terminierung gilt die Formel.

Wenn ich nun eine Aufgabe wie in dieser Übung erhalte: "Prove partial correctness for method by providing a loop invariant"

Was ist nun genau zu tun. Gebe ich nur die Invariante(n) (ohne oder mit diverges true für partial correctness?) an? um dann im 2. Schritt bei "Is total correctness possible to prove" durch die Angabe eines decreasing ...zu zeigen, dass eine Möglichkeit der Terminierung existiert, und damit total correctness erfüllt ist?

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Exercise 6 - Partial Correctness vs. total correctness

Beitrag von yourmaninamsterdam »

Du verstehst das völlig richtig.

Antworten

Zurück zu „Archiv“