Moderne Entwicklungsansätze wie die modellbasierte Softwareentwicklung benötigen formale Grundlagen, um beispielsweise eine automatische Ableitung von Implementierungen aus Modellen zu ermöglichen, oder um die Eigenschaften sicherheitskritischer Systeme nachzuweisen. Formale Sprachen und Grammatiken sind die Grundlage für Programmiersprachen, Übersetzer, und eine Vielzahl anderer textverarbeitender Systeme. Formale Logiken, insbesondere Aussagen- und Prädikatenlogik, sind die Grundlage der Informatik. Sie ermöglichen z.B. die eindeutige und verifizierbare Spezifikationen von funktionalen Eigenschaften eines Programms oder Programmsystems. Rewrite-Techniken erlauben die Beschreibung von Äquivalenzen und deren Anwendung, etwa zur Transformation von Programmen von einer abstrakteren in eine konkretere Form. Formale Beweistechniken erlauben es, sichere Aussagen über Programmsysteme und Techniken zu machen und zu belegen. In der Veranstaltung werden diese Grundlagen erarbeitet und Anwendungen im Software Engineering aufgezeigt. |