Dynamische Semantik

• operational:

  beschreibt Wirkung von Anweisungen durch Änderung des Programmzustandes

• denotational:

  ordnet jedem (Teil-)Programm einen Wert zu, Bsp: eine Funktion (höherer Ordnung).

  Beweis von Programmeigenschaften durch Term-Umformungen

• axiomatisch (Bsp: Hoare-Kalkül):

  enthält Schlußregeln, um Aussagen über Programme zu beweisen