Qualifikationsziele: Die Studentinnen und Studenten sind in der Lage – Algorithmen zustandsbezogen zu spezifizieren, – gut strukturierte imperative Programme zu entwickeln, – imperative Programme hinsichtlich ihrer Komplexität zu analysieren und – Eigenschaften imperativer Programme formal zu beweisen.

Inhalte: Grundlagen der Berechenbarkeit: – universelle Registermaschinen – Syntax und operationelle Semantik imperativer Programmiersprachen Formale Verfahren zur Spezifikation und Verifikation imperativer Programme: – Bedingungen auf dem Zustandsraum (assertions) – Hoare-Kalkül, partielle Korrektheit, Termination Konzepte imperativer und objektorientierter Programmierung (Java): – primitive und zusammengesetzte Datentypen – Methoden (Prozeduren und Funktionen), Parameterübergabe, Überladung – Module, Klassen, Objekte – Klassenhierarchien, Vererbung, abstrakte Klassen, Schnittstellen Programmiermethodik: – schrittweise korrekte Programmentwicklung – Teile und Herrsche – Backtracking Analyse von Laufzeit und Speicherbedarf: – O-Notation – Umwandlung von Rekursion in Iteration – Analyse von Such- und Sortieralgorithmen.