Denotationale Semantik (II)

Semantik des Programms P ist Menge der Spuren von P .

• Spur = eine Folge von Paaren von Zustand und Aktion,
• ein Zustand ist eine Belegung der Prädikatsymbole,
• jede Aktion zerstört alle Zustandsinformation.

Satz: Diese Spursprachen (von goto- und while-Programmen) sind regulär.

Beweis: Konstruktion über endlichen Automaten.

• Zustandsmenge = Prädikatbelegungen × Anweisungs-Nummer
• Transitionen? (Beispiele)

Damit ist Spur-Äquivalenz von Programmen entscheidbar.
Beziehung zu tatsächlicher Äquivalenz?