RainerH88

Guten Abend , kennt sich hier jemand mit Programmverifikationen aus? Ich habe hier folgenden code: x := a; y := b; p := 0; while x > 0 do begin p := p + y; x := x - 1; end; die Inv müsste lauten: x*y+p=a*b und die Post-Bedingung: p=a*b wie aber muss die Pre-Bedingung aussehen? a und b >0 und p=0? Gruß Rainer

alles klar, ich hab meinen Automaten dementsprechend umgewandelt. Eine Frage hab ich noch zu den Endzuständen. Was ist das eigentlich genau. Sind das die Zustände, wo es passieren kann das sie keine ebene mehr weiter kommen bzw sich in einer endlosschleife verharren? mfg rainer

ööhm, seid ihr mir böse, wenn ich gerade total verwirrt bin xD was ist denn denn nun mit dem teil? Rein nach der Logik sollte er doch funktionieren. Ich frage mich nur ob meine Endzustände auch wirklich endzustände sind. mfg Rainer

ah okay, dann würde ich also noch schleife von start auf start legen, die alle anderen eingaben abfängt. Würde das reichen? mfg Rainer

Hi, vielen Dank für die schnelle Antwort. Aber der Automat darf doch auch jede (der zulässigen Eingaben w,x,y) Eingabe akzeptieren, oder? bzw. es ist nicht Pflicht, dass er unbeingt auch mit w anfangen muss. es könnte auch xxyxw heißen mfg Rainer

Hi leute, schönes Forum habt ihr hier Kennt sich hier jemand mit DEAs aus? Ich hab mal einen Ablauf gestaltet in dem geprüft werden soll, ob zwischen einem w und einem y ein bzw. zwischen einem y und einem w ein x vorkommt. Kann mir einer sagen ob dieser Algorithmus so richtig ist? Bsp: wwwxy,wxxxyy sind möglich, wwyybw hingegen nicht. Würde mich sehr freuen, wenn mir jemand helfen könnte. mfg Rainer