Semantik von Programmiersprachen

Objective

Ziel der Vorlesung ist es, die grundlegenden Techniken zur präzisen Definition der Semantik einer Programmiersprache zu verstehen und diese Techniken anzuwenden auf Probleme wie die Äquivalenz verschiedener Sprachbeschreibungen, Programmkorrektheit oder die Korrektheit von Programmtransformationen.

Content

Formale Semantiken von Programmiersprachen liefern ein mathematisches Modell der Programmausführung. Sie bilden die Grundlage für den Nachweis von Eigenschaften sowohl der Programmiersprache, zum Beispiel Typsicherheit, als auch von Programmen, beispielsweise mittels Verifikation. Darüber hinaus spielen Semantiken bei der Implementierung von Programmiersprachen eine wichtige Rolle: Interpreter können zum Beispiel automatisch aus einer formalen Semantik generiert werden. Daher gehört die Beschreibung und Nutzung formaler Semantiken zum Handwerkszeug von Informatikern, die sich fundiert mit Programmierung und Programmiersprachen befassen. Diese Vorlesung gibt eine grundlegende Einführung in die Semantik von Programmiersprachen. Sie erläutert die operationelle, denotationale und axiomatische Semantik einer Sprache sowie deren Beziehungen untereinander. Darüber hinaus werden typische Anwendungen dieser Semantiken besprochen und an Beispielen illustriert.

Resources