Automatischer Korrektheitsnachweis von Programmtransformationen

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

Untersucht werden Semantiken verschiedener – insbesondere nebenläufiger und nichtdeterministischer – Programmiersprachen (repräsentiert durch Programmkalküle) auf der Basis der kontextuellen Gleichheit, die wiederum auf einer operationalen Semantik aufsetzt. Informell: zwei Programme sind gleich, wenn man keinen Unterschied bzgl. Terminierung / Nichtterminierung „beobachten“ kann, bei allen möglichen Verwendungen. Diese Gleichheitsdefinition ist von Interesse, da sie maximal ist und fast immer anwendbar ist, auch dann noch, wenn andere Semantik-Formalismen versagen oder zu restriktiv sind. Ziel ist die Automatisierung des Korrektheitsnachweises von Programmtransformationen. Der algorithmische Kern ist die Berechnung der Überlappungen von Auswertungsregeln und Transformationsregeln in Analogie zum Berechnen der kritischen Paare nach Knuth-Bendix. Diese Methode soll so allgemein umgesetzt werden, dass diese für viele Programmkalküle verwendbar ist, und somit auch für andere Forschergruppen von Interesse ist.