vereinfachtes Modell, damit Eigenschaften entscheidbar werden (sind die Programme P1, P2 äquivalent?)
Syntax: Programme
Beispiel:
while (B && !C) { P; if (C) Q; }