Ein monadenbasierter Programmlogikbaukasten für generische und heterogene Seiteneffekte (PLB).

点击翻译按钮获取中文摘要

Die steigenden Anforderungen an die Sicherheit von Software bringen einen erhöhten Bedarf nach formaler Verifikation mit sich. Die dazu benötigten Programmlogiken sollten flexibel, handhabbar und modular sein, um sie einfach erweitern oder auf neue, insbesondere domänenspezifische Programmiersprachen anpassen zu können. Dies wird erschwert durch die vielfältige Art von benötigten Seiteneffekten, wie etwa Zustandsabhängigkeit, Ausnahmen, Ein-/Ausgabe oder Nebenläufigkeit. Ziel von PLB ist die Entwicklung eines Baukastens für Semantik, Metatheorie und Programmlogikentwurf, der die strukturierte Kombination solcher Effekte und der sie modellierenden Logiken unterstützt. Das etablierte Mittel zur einheitlichen Repräsentation und Verkapselung von Seiteneffekten in der modernen Programmiersprachensemantik sind Monaden; Monaden erlauben ferner bereits eine kompositionale Spezifikation von Seiteneffekten, in der verschiedene Effekttypen nach einem Baukastenprinzip kombiniert werden können. In PLB wird dieses Baukastenprinzip auf ein System von generischen Programmlogiken ausgedehnt, so dass jedem kombinierten Effekt eine kombinierte Programmlogik zur Seite gestellt wird, die natürliche und effektive Ausdrucksmittel zur Verifikation entsprechender seiteneffektbehafteter Programme bietet. Der Baukasten wird in einer Fallstudie evaluiert, in der eine Sprache zur Gebäudesteuerung modelliert wird.