beschreibt Wirkung von Anweisungen durch Änderung des Programmzustandes
enthält Schlußregeln, um Aussagen über Programme zu beweisen
ordnet jedem (Teil-)Programm einen Wert zu, Bsp: eine Funktion (höherer Ordnung).