Student02
-
Gesamte Inhalte
3 -
Benutzer seit
-
Letzter Besuch
Inhaltstyp
Profile
Forum
Downloads
Kalender
Blogs
Shop
Beiträge von Student02
-
-
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
Brauch Hilfe bei Turing Maschinen
in Prüfungsaufgaben und -lösungen
Geschrieben
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