Aufgabe 8.2.1: "Primitive Berechnungsschritte" und While

Erich
Mausschubser
Mausschubser
Beiträge: 57
Registriert: 17. Okt 2010 13:29

Aufgabe 8.2.1: "Primitive Berechnungsschritte" und While

Beitrag von Erich »

Abend,

Also ich sitze grad an obiger Aufgabe und will nun die Regeln für While-Kommandos definieren, ich habe folgende/s Frage/Problem:

Wenn ich ein Kommando der Form <while b do c od, phi> habe, wie sieht hier ein "primitiver" Berechnungsschritt aus, wenn wir jetzt mal davon aus gehen, dass
c = c1;c2;...;cN; ( wobei ci jetzt durchaus als primitiv angenommen wird ) ?

<...,phi> -->1 <while b do c' od, phi'>, wobei hier c' = c2;c3;..;cN; ist, ist mir als erstes in den Sinn gekommen, formal bedeutet es aber, dass das Programm für jedes Teilkommando in c eine komplett neue Schleife startet, was natürlich Humbug ist.

<...,phi> -->1 <c',phi'> sah schon vielversprechender aus, würde aber auch bedeuten, dass sobald in die Schleife gesprungen wird, es aufhört eine Schleife zu sein und einfach c durcharbeitet, salopp gesagt. Ich weiß nicht, wie ich zusätzlich in der Konklusion in der uns gegebenen Notation ausdrücken soll, dass <cN,phiN> -->1 <while b do c od, phiM>.

Oder soll ich hierbei davon ausgehen, dass ein primitiver Schritt mit einer Schleife hier einen Schleifendurchlauf bedeutet? Würde natürlich vieles einfacher machen.

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Aufgabe 8.2.1: "Primitive Berechnungsschritte" und While

Beitrag von dschneid »

Versuch mal folgenden Denkansatz: Wenn die Bedingung einer Schleife zu true auswertet, dann soll intuitiv gesehen eine neue Iteration der Schleife beginnen. Anders gesprochen: Es wird in die Schleife gesprungen, um den Body der Schleife noch einmal auszuführen.

Jetzt kannst du dir überlegen, wie du das formal modellieren kannst. Denk dabei daran, dass das Statement in einem Urteil angibt, was noch auszuführen bleibt, und dass dieses Statement nicht immer nur kleiner werden muss.

Antworten

Zurück zu „Archiv“