towards symbolic execution into normal form

Hallo Alexander,

ich habe mal einen Versuch gestartet, wie ST0 in eine eindeutige Zuweisungsform gebracht werden könnte.
Dazu habe ich symbolic execution von vorne her verwendet. Das heißt, dass alle Tabelle gehalten wird mit allen bisherigen Zuweisungen, die dann durch Ablaufen des Programmes aktualisiert wird.

Das eine Beispiel, das dabei ist, ergibt eine stimmige Ausgabe.

Ich hab einen synthetischen neuen Typ von Expressions aufgenommen, der von der Form
CASES(cond -> val; cond2 -> val2; ELSE -> valElse) ist. Die conditions müssen disjunkt sein. Die Semantik ist, denke ich, selbsterklärend.

Beste Grüße

Mattias