SW-Verfikation, induktiver Beweis
-
Ich soll induktiv zeigen (structural operational semantics), dass:
[p;q][e]sigma[/e] = [q][p][e]sigma[/e]für alle Programme p und q sowie für alle Stati σ gilt.
Steh' aber gerade vollkommen daneben. Worüber soll ich hier etwas induktiv zeigen? Die Programmlänge erweitern? Für mich sieht das irgendwie nur nach anderer Notation aus?!
MfG SideWinder
-
OT: "Stati" gibts nicht. Du meinst "Status" (mit langem u).
-
Michael E. schrieb:
OT: "Stati" gibts nicht. Du meinst "Status" (mit langem u).
Danke, dachte die MZ wäre anders, scheint aber nicht so zu sein. Hilft mir beim Beweis aber auch nur sehr geringfügig weiter
MfG SideWinder
-
SideWinder schrieb:
Steh' aber gerade vollkommen daneben. Worüber soll ich hier etwas induktiv zeigen? Die Programmlänge erweitern? Für mich sieht das irgendwie nur nach anderer Notation aus?!
Evtl. Induktiv über alle Programmkonstrukte. Zuerst die elementaren, nicht weiter zerlegbaren Befehle. Dann die höheren (Schleifen, etc.)
Kann aber auch total danaben liegen. Das ist alles schon sehr lange her.