vereinfachtes Modell, damit Eigenschaften entscheidbar werden (sind die Programme P1, P2 äquivalent?) Syntax: Programme Aktionen, Zustandsprädikate (in Tests) Sequenz/Block, if, goto/while. Beispiel: while (B && !C) { P; if (C) Q; } 2015-01-26
Syntax: Programme
Beispiel:
while (B && !C) { P; if (C) Q; }