Also ich arbeite hier gerade ein Buch durch - es geht um Spezifikation...

"In einer Spezifikation {P}A{Q} gehen wir immer von der Terminierung des Algorithmus A aus. Wenn A nicht terminiert, so erfüllt er trivialerweise die Spezifikation."
(das ganze für ein Q <> false, sonst wäre es ja klar)

Stimmt das so? Ein nicht terminierender Algorithmus kommt doch nie bei {Q} an!?

Ich hoffe, hier kann jemand Aufklärung leisten!

Hi,

wenn eine Spezifikation zu einen nicht terminierenden Algorithmus paßt, dann doch nur wenn in der Spezifikation selbst keine Terminierung erfolg.

Normalerweise wird in der Spezifikation die Terminierung mittels mathematischem Modell eindeutig bestimmt.

Selbst bei Berechnungen von Nährungswerten, deren Algorithmen nicht terminierend sind, wenn das Ergebnis irrational ist, muß ein Schlußstrich gesetzt werden (z.B. max. Genauigkeit).

Falls das nicht in der Spezifikation berücksichtigt wird, ist die Spezifikation fehlerhaft, denn sie verstoßt gegen die allgemeinen Anforderungen an einen Algorithmus (Terminierung, Korrektheit,...).

Man könnte höchstens formulieren, daß das Ergebnis des nicht terminierenden Algorithmus im Unendlichen liegt, doch dabei "beißt sich die Katze in der Schwanz".

(In Haskel gibt es die Möglichkeit mit unendlichen Listen zu arbeiten, evtl. kann dir das auch schon weiterhelfen.)

MfG BJ

Danke für die Antwort!
Wenn ich dich richtig verstanden habe, dann habe ich also Recht und der zweite Satz muss da lauten:
"Wenn A nicht terminiert, so erfüllt er trivialerweise nicht die Spezifikation."

Jo, genau das.

Nachdem, was ich in den Vorlesungen zu Algorithmen und Datenstrukturen gehört und gelernt habe, ist bei einer Spezifikation die Terminierung immer eindeutig bestimmt. (Auch wenn man den Algorithmus mit beispielsweiser einer Hilfsvariable zum terminieren zwingen muß).

MfG BJ

Okay. Vielen Dank für deine Hilfe.
Dachte schon, ich hätte was Grundlegenes nicht verstanden...