Denotationale Semantik (II)

Semantik des Programms P ist Menge der Spuren von P.

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

Beweis: Konstruktion über endlichen Automaten.

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



Johannes Waldmann 2013-01-28