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?



2010-02-04