Frage zur Kalkülerstellung (KeY)

null
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Frage zur Kalkülerstellung (KeY)

Beitrag von null »

Hallo!

Ich versuche gerade die y = x++ Regel darzustellen und wundere mich über die Herangehensweise von KeY. So sieht etwa meine Prämisse aus:

...<y = x; x=x+1; rest>...

KeY macht folgendes:

...<int j = x; x = (int)(x+1); y = j; rest>...

Ist meine Variante falsch?
Warum geht KeY den Umweg über eine lokale Variabel j?

Vielen Dank

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Frage zur Kalkülerstellung (KeY)

Beitrag von yourmaninamsterdam »

KeY gibt die Semantik des Inkrement-Operators wieder: Der Ausdruck x++ bedeutet: erhöhe den Wert einer Variable x um 1 und gib den ursprünglichen/alten Wert zurück. Wenn das jetzt Teil einer Zuweisung ist, wird anschließend zugewiesen. Das macht KeY:
  1. Sich den Wert merken, damit er später zurückgegeben werden kann.
  2. Den Wert von x um 1 erhöhen.
  3. Den alten Wert zurückgeben (und zuweisen).
Deine Lösung ist tatsächlich nicht korrekt. Das zeigt der Spezialfall x = x++.

Antworten

Zurück zu „Archiv“