Denotationale Semantik (II)

Semantik des Programms P mathend000# ist Menge der Spuren von P mathend000#.

• Spur = mathend000# 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 = mathend000# Prädikatbelegungen × mathend000# Anweisungs-Nummer
• Transitionen? (Beispiele)

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