Hallo,
ich brauche dringen eine Hilfe zum Thema FGI3, weil mit der Zeit bin sehr knapp und die Antwort weiss nicht, mit Hilfe Axiomatische Semantik soll es gezeigt werden, dass zwei Programme Semantisch Äquivalent sind, die Programme sind sehr kurz, sehr lieb und nett von alle, die bei mir sich melden: 7reza@informatik.uni-hamburg.de
LG

Welche Programme?

die sind nur zwei Programmfragmente.

Also ich bin kein Experte was Semantik angeht aber bei der axiomatischen Semantik hast du ja eigentlich immer dieses Tripel {Vorbedingung}Programm{Nachbedingungen} und dann hast du ein Kalkül, wie du Tripel in andere Tripel überführen kannst. Wenn du nun zeigen sollst, dass zwei Programme semantisch Äquivalent müsste es ja eigentlich reichen, dass die Programme unter den gleichen Vorbedingungen immer die gleichen Nachbedingungen einhalten (ohne Gewähr). Vielleicht nützt das ja schon etwas. Mehr Hilfe wirst du wohl ohne weitere Informationen nicht erhalten.

es geht um diese zwei Programmen:
Programmfragment1:   x, y Integer
                                     x:= x+y;
                                     y:=x-y;
                                     x:= x-y;
Programmfragment2:   x, y, z Integer
New  var           z:=x    in   (  x:=y;
                                        Y:=z);
wie soll ich es zeigen? danke.

Was hast du dir angeguckt? Was hast du versucht? Was hast du nicht verstanden? Ein bisschen Eigeninitiative ist schon notwendig.

ich habe so was gedacht ist das richtig?
{P1}S1{Q1}
{P2}S2{Q2}
Semantisch Äquivalent. d.h. P1=P2 dann Q1=Q2, dann:
Programm1: x:=x+y, y:=x-y , x:=x-Y
P:{x= b and y=c} S:{ x:=x+y, y:=x-y , x:=x-y} Q: {x=b , y=c}
P’1: { x:=b and y:= c} {x:= x+y} Q1:{x:= b+c, y:=c}
Q1:{x:= b+c, y:=c} { y:= x-y} Q2{x:=b+c, y:=b}
Q2:{x:=b+c, y:=b} {x:=x-y } Q’3{x=b , y=c}

P’1: { x:=b and y:= c} { x:=x+y, y:=x-y , x:=x-y} Q’3 {x=b , y=c}
Programm2:
P:{ x= b and y=c} S:(z:=x; x:=y ; y:=z) Q:{ x=c and y=b}
P1: { x=b and y=c} {z : = x} Q1: {z=b and y=c}
Q1: {z=b and y=c} {x : = y} Q2: {z=b and x=c}
Q2: {z=b and x=c} {y := z} Q3:{y=b and x=c}
=> P1: { x=b and y=c} {z:=x,; x:=y; y:=z} Q3:{y=b and x=c}
Result: beide Programmen sind nicht Äquivalent, weil unter gleiche Vorbedingung wurde nicht die gleichen Nachbedingung erfüllt.

sorry, ich habe am Ende programm1 einen Fehler gemacht, es ist so:
P’1: { x:=b and y:= c}    { x:=x+y,  y:=x-y ,  x:=x-y}  Q’3 {x=c , y=b}
P1: { x=b and y=c}       {z:=x,; x:=y;  y:=z}              Q3:{y=b and x=c}  
d.h, beide Programmen sind Semantisch Äquivalent, ist das richtig? Danke