AL um for-Schleife erweitern

[Lukas]

bei einem beispiel von der letzten prüfung soll man die sprache AL um eine for-schleife erweitern, genaue angabe siehe hier (http://www.logic.at/lvas/thinf1/angaben/ti1v024.pdf).

weiss jemand wie das geht? hab keine ahnung wie man das machen sollte.

[edit] hat sich erledigt.

[Lukas]

zur for-schleife gibts jetzt eh schon die lösung, aber ich bin mir noch immer nicht sicher ob ich verstanden hab wie man die semantik erweitert.

ich hab versucht zwei ähliche beispiele aus dem prüfungsordner zu machen, wär nett wenn mir jemand sagen könnte ob die lösungen stimmen.

1) Semantik von AL um repeat-schleife repeat α until B erweitern.

lösung: MAL(I, repeat α until B) =
= MAL(I, α ) für MPL(I,B) = false
= MAL(MAL(I,α ) repeat α until B) für MPL(I,B) = true

2) wie 1), loop α exitwhen B β endloop
= MAL(I, α ) falls B = true
= MAL(MAL(I, α ) loop α exitwhen B β endloop) falls B = false

bin mir vor allem wegen dem β beim zweiten nicht sicher. bei meiner definition wird das beta glaub ich nie ausgeführt, ich weiss aber nicht wie ichs anders definieren könnte.

[qmp]

2) wie wärs damit
MAL(MAL(MAL(I, a ), ß) loop a exitwhen B ß endloop) falls B = false

1) hab ich auf while zurückgeführt:
MAL(I, repeat a until B) =
= MAL(MAL(I,a), while -B do a)

aber ich denke deines stimmt auch

[Lukas]

ja das zweite könnt so stimmen, danke :)

1) stimmt aber bei dir glaub ich nicht. while -B do α bricht ab wenn B=true, repeat α until B wird noch einmal ausgeführt wenn B=true weil die bedingung erst am ende überprüft wird .

[qmp]

deswegen ist ja auch das MAL(I,a) drinnen, also a wird mind. einmal ausgeführt

MAL(MAL(I,a), while -B do a)
^^^^^^^^^