Formale, mechanisch unterstützte Fundierung aspektorientierter und kollaborationsbasierter Sprachen

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

Die neuen Sprachparadigmen Aspektorientierung und Kollaborationsbasierung zielen u.a. auf die Entwicklung von sicherheitskritischen Anwendungen ab, von denen die strenge Einhaltung von Qualitätseigenschaften wie Safety, Security und Reliability gefordert wird. Die entsprechenden Sprachkalküle beenden sich noch in der Entwicklung und sind teilweise nicht wohlverstanden. Es herrscht ein regelrechter Wildwuchs\ an Erweiterungen um neue Sprachelemente und Programm-Konstruktoren. Ziel des Projekts ist es, mit interaktiven Theorembeweisern relevante Eigenschaften wie z.B. Typsicherheit auf den neuen Sprachparadigmen nachzuweisen oder zu widerlegen. Hierzu soll zuerst eine formale Semantik für die neuen Sprachen definiert werden, mit deren Hilfe wir eine kritische Betrachtung der einzelnen Sprachelemente durchführen können. Es soll rigoros nachgewiesen werden, dass die auf diese Elemente reduzierten Sprachen die geforderten Eigenschaften aufweisen. Ein einfaches Beispiel für eine Spracheinschränkung ist das Verbot von Sprachmitteln, die offen Kapselungsvereinbarungen brechen wie privileged-Aspekte in der aspektorientierten Sprache AspectJ. Weniger trivial ist es z.B. zu entscheiden, was von geschachtelten Konstrukten wie around-Advices in AspectJ verlangt werden muss, damit sie die Typsicherheit nicht verletzen. Die aktuellen Implementierungen der Sprachen vernachlässigen bisher derartige Probleme. Wir verwenden den konstruktiven Theorem-Beweiser Coq für Higher Order Logic. Aus den mechanisierten Beweisen können wir automatisch verifizierte Compiler und Typchecker erzeugen, die als Referenzimplementierungen und Test-Orakel für in der Entwicklung stehende Compiler und Typchecker dienen können.