Universe Types - Topologie, Kapselung, Generizität und Tools

Mehrere veranderbare Referenzen auf ein Objekt geben objektorientierten Programmiersprachen Ausdruckstarke, verkomplizieren allerdings das Programmverstandniss und verunmoglichen verschiedenste formale Beweise von Programmen. Als Losungsmoglichkeit fur diese Probleme bieten sich Ownership-Typsysteme an, die den Speicher hierarchisch strukturieren und die moglichen Referenzen und deren Effekte beschranken. Generic Universe Types sind ein typsicheres, leichtgewichtiges Ownership-Typsystem fur typgenerische objektorientierte Programmiersprachen, das die OwnershipTopologie klar von der Owner-as-Modifier-Kapselungsdisziplin trennt und von einer umfassenden Menge an Tools unterstutzt wird. In meiner Doktorarbeit gebe ich zuerst einen ausfuhrlichen Uberblick uber die Problemstellung und definiere dann eine Programmiersprache und eine entsprechende Laufzeitumgebung. Danach prasentiere ich das GUT Typsystem das die OwnershipTopologie sicherstellt und darauf aufbauend separate Regeln um die Owner-as-Modifier-Kapselungsdisziplin sicherzustellen. Die Doktorarbeit formalisiert die Eigenschaften des Systems und beweist ausfuhrlich deren Gultigkeit. Weiters beschreibe ich die von mir entwickelten Tools, namlich verschiedene Typchecker und Inferenz-Tools. In dieser Kurzfassung meiner Doktorarbeit stelle ich den Problembereich dar und prasentiere anhand von Beispielen die Grundgedanken des Typsystems.