Verifikation

[Student02]

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

[TDM]

Wenn x und y Elemte von Z sind und Elemente von Z addiert und subtrahiert werden, können nur Elemente von Z rauskommen. O.o

[Klotzkopp]

Wenn x und y Elemte von Z sind und Elemente von Z addiert und subtrahiert werden, können nur Elemente von Z rauskommen. O.o

Ich bin sicher, es geht ihm darum:

{x=max{A,B}, y=min{A,B}}

@Student02:

Das ist ein ziemlich weites Feld, es gibt mehrere Möglichkeiten der Verifikation. Welche Ansätze wurden in der Vorlesung denn vermittelt?

Ansonsten gibt's hier ein paar allgemeine Infos: http://en.wikipedia.org/wiki/Verification

[TDM]

Ich bin sicher, es geht ihm darum:

Ist doch das gleiche...

{Element von Z = max{Element von Z, Element von Z}, Element von Z = min{Element von Z, Element von Z}}

So werden doch beide Werte wieder den ursprünglichen zugeordnet weil nur mit diesen gerechnet wurde...

[Klotzkopp]

So werden doch beide Werte wieder den ursprünglichen zugeordnet weil nur mit diesen gerechnet wurde...

Das ist kein formaler Beweis, und obendrein Quatsch. Wenn ich mit zwei Werten rechne, kann dabei auch etwas ganz anderes herauskommen.

[TDM]

Das ist kein formaler Beweis, und obendrein Quatsch. Wenn ich mit zwei Werten rechne, kann dabei auch etwas ganz anderes herauskommen.

gut das ist quatsch

hab mich nur auf den fall x>0 festgelegt:

am anfang ist x = x - y

wenn das größer 0 ist wird das wieder umgetauscht: x = x+y

vergessen schleife zu berücksichtigen...

was soll der algorithmus eigentlich zeigen ?

[Klotzkopp]

vergessen schleife zu berücksichtigen...

Eine Schleife seh' ich jetzt nicht...

was soll der algorithmus eigentlich zeigen ?

Gar nichts. Es geht darum, formal zu beweisen, dass er tut, was er soll.

[TDM]

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}}

nix schleife ?

Es geht darum, formal zu beweisen, dass er tut, was er soll.

Wenn er nichts zeigt dann kann man das doch nichts beweisen ?

er verändert die werte oder lässt diese gleich O.o

ich weis schon warum ich bei sowas immer krank war :floet:

[Der Kleine]

Habe zwar keine Ahnung von Informatik, aber mathematisch gesehen würde ich zu einer vollständigen Fallunterscheidung neigen.

Es gibt die Möglichkeiten:

A=B

A>B

und A<B

Was passiert mit den Zuordnungen für jeden Fall und bleibt als Endergebnis stehen? - Dette ist dann einfach.

Es ist schon so, daß x=max{A;B} und y=min{A;B} darstellt.

*abgesehen von der korrekten Notation dürfte auch die Informatik keiner anderen Logik unterliegen, als die Mathematik*

[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

[allesweg]

nix schleife ?

Ja, nix Schleife - nur ein Block. Schleife = Wiederholung.

[MikeVader]

Ich kann dir leider nicht weiterhelfen bei denem Problem, interessiere mich aber fuer dieses Gebiet und waere dankbar wenn jemand gute Quellen oder Buecher zu diesem Thema angeben koennte. War mir bisher nicht bewusst, dass es formale Beweise fuer Algrorithmen gibt und moechte mich in dieses Thema einarbeiten.

Kannte bis jetzt nur formale Beweise fuer die Komplexitaet bzw Aufwand von Algroithmen.

P.S. Der Wikipedia-Link war schon sehr informativ, jedoch ist vorallem erklaert was es genau ist und weniger wie man es einsetzt und leider ist die Publikationsliste etwas zu umfangreich um eine gute Auswahl zu treffen.