Student02

Hallo, kann mir jemand erklären wie man für eine beliebige TM entscheiden kann, ob sie zum Beispiel bei der Eingabe von dem &-Zeichen anhält? Mfg

Hi, erst mal danke für eure Antworten, ich soll das mit der "Hintereinanderausführungsregel" und der "Zuweisungsregel" beweisen! Also: Wenn {P}S1{R} und {R}S2{Q} dann {P}S1,S2{Q} (Hintereinanderausführungsregel) und Wenn P => Q[v/t] dann {P}v:=t{Q} (Zuweisungsregel) Ich denke man muss das Programm erstmal in zwei Programme aufteilen, wegen dem IF-Satz, also für (x<0) und (x>=0). Dann muss man jeweils S1 und S2 definieren und dann R und R' bestimmen usw. Bis man das Programm Verifiziert hat. Ich hätte jetzt für S1 = x:=x-y; und für S2 = y:=x+y;x:=y-x; genommen. Hieraus erhält man jetzt zwei Behauptungen: {x=A, y=B}S1{R} und {R}S2{x=max{A,B}, y=min{A,B}} bzw. {x=A, y=B}x:=x-y;{R} und {R}y:=x+y;x:=y-x;{x=max{A,B}, y=min{A,B}} So, jetzt müsste man irgendwie R bestimmen, aber da komme ich nicht weiter. Ich hoffe ihr habt eine Idee.. Mfg

Hi, ich schreibe nächste Woche eine Nachschreibeklausur in Info, in der es unter anderem auch um die Verifikation von Programmcode geht. Allerdings habe ich nicht viel Ahnung davon. Aber vielleicht könnt ihr mir ja helfen. Der Code sieht z.b. so aus: A,B ist Element von Z {x=A, y=B} x:=x-y IF x<0 THEN BEGIN y:=x+y; x:=y-x; END ELSE x:=x+y {x=max{A,B}, y=min{A,B}} Wie beweise ich sowas am besten? Da gibt es ja auch verschiedene Wege. Man kann ja von vorne oder von hinten anfangen? Wäre für Hilfe sehr dankbar. Vielleicht kennt ja auch jemand eine Homepage wo das gut erklärt wird. Mfg