wp Kalkül

[JeNeSaisPas]

Hallo zusammen, brauche dringend einen Tipp zur folgenden Aufgabe: bestimmt das wp Kalkül wp(A,Q):
alle Variablen sind vom Typ int

A: x = y++ + 1 ; y += ++u − x++ + e ;

und Q: u < y

meine lösung wäre jetzt wie folgt:

wp(„x = y++ + 1; y += ++u – x++ + e;“,u < y)
--> wp("y = ++y + ++u – (y++ + 1) + e;", u < y)
--> wp("y = ++u + e;", a < y) = y > u;


kann mir irgendjemand sagen ob das stimmt? ???:L

 

[Marco13]

Hallo Я не знаю wp-Kalkül kannte ich nicht, aber Vor- und Nachbedingungszeug halt schon. Was ist denn das 'a' dort - und wo kommt das her?

 

[JeNeSaisPas]

sorry war ein tippfehler es muss heißen Q: u < y
kannst du mir weiterhelfen? bin schon am verzweifeln, hab noch mehr aufgaben dieser art und wüsste gern ob ich auf dem richtigen weg bin

 

[Marco13]

Hm. Diese Kalkülartige Schreibweise ist für mich eher unübersichtlich, und die wilde Mischung aus ++x und x++ zielt wohl genau darauf ab (wenn jemand in der Realität solchen Code schreiben würde... :autsch: )... Aber wenn ich versuchen sollte, aus der Nachbedingung die WP zu berechnen, ganz unbedarft, pragmatisch, würde ich erstmal versuchen, das auseinanderzupflücken

x = y++ + 1; 
y += ++u − x++ + e;

Die ganzen ++ und += auflösen

x = y + 1; 
y = y + 1
y = y + 1 + u − (x) + e;
u = u + 1
x = y + 1

Einsetzen

y = y + 1
y = y + 1 + u − (y + 1) + e;
u = u + 1

Einsetzen

y = y + 1 + 1 + u − (y + 1) + e;
u = u + 1

Ausrechnen

y = 1 + u + e;
u = u + 1

Bedingung

// u < y 
(u + 1) < (1 + u + e) <=>
0 < e

Aber Achtung: Ich habe KEINE Ahnung, ob das richtig oder sinnvoll ist, geschweige denn wie man das jetzt in die Kalkülform presst... auch die Uhrzeit beachten, die wird morgen sicher als 1A Ausrede herhalten, wenn ich nach dem Kaffee erkenne, was für einen Unfug ich hier geschrieben habe :smoke: Aber um mich zumindest selbst ansatzweise zu überzeugen, hab' ich mal das hier geschrieben

class WpTest
{

    public static void main(String args[])
    {
        for (int y=-10; y<=10; y++)
        {
            for (int u=-10; u<=10; u++)
            {
                for (int e=-10; e<=10; e++)
                {
                    doit(y,u,e);
                }
            }
        }
    }

    public static void doit(int y, int u, int e)
    {
        int x = y++ + 1;
        y += ++u - x++ + e;
        if (u < y) System.out.println("! "+y+" "+u+" "+e);
        else       System.out.println("  "+y+" "+u+" "+e);
    }

}

Und da sieht es so aus, als ob die ganze Zahlen ziemlich wurscht wären, aber die Nachbedingung immer erfüllt ist, wenn e>0 ist...

Mal schauen, was Leute dazu sagen, bei denen die Uni noch nicht ganz so lange her ist ....

 

[JeNeSaisPas]

vielen vielen Dank nochmal klingt auf alle Fälle logisch glaub aber fast dass sich sonst niemand für dieses "spannende" Thema interessiert

 

[Marco13]

Ich finde schon dass das ganz interessant (und auch wichtig) ist. In bezug auf die "nicht-formale" Frage: Wenn die Funktion dies-und-das liefern soll, was muss ich dann oben reinstecken? Das mal formal durchzuexerzieren ist wohl nur eine kleine Übung, und schärft vielleicht das Bewußtsein für die Möglichkeiten. Die reichen dann eben bis hin zu vollkommen automatischer formaler Programmverifikation. Und sowas brauch man auch, weil das in der Form ja kein Mensch (außer Infostudenten im ersten Semester ) per Hand macht. Ob es nicht sinnvoller wäre, dieses ++- und +=-Gekrampfe, was AUCH in der Realität kein Mensch macht, und was nur dem fragwürdigen Zweck dient "diese Übungsaufgabe schwerer zu machen", einfach bleiben zu lassen, und stattdessen mal ein realistischeres Beispiel (speziell mit einer Schleife) als Übung durchzuspielen, sei mal dahingestellt....