C++ ist typsicher? Garantiert!
Abstract:
Wir präsentieren eine operationelle Semantik mit Typsicherheitsbeweis für Mehrfachvererbung in C++, formalisiert im und maschinengeprüft durch den Maschinenbeweiser Isabelle/HOL. Die Typsicherheit des Vererbungsmechanismus von C++ war
lange offen. Der nun vorliegende Beweis erhöht das Vertrauen in die Sprache, erzeugt aber auch neue Einsicht in die Problematik des C++-Vererbungsmechanismus. Er öffnet die Tür für weitergehende Beweise, die bisher unerreichte Sicherheitsgarantien für C++-Programme liefern.
lange offen. Der nun vorliegende Beweis erhöht das Vertrauen in die Sprache, erzeugt aber auch neue Einsicht in die Problematik des C++-Vererbungsmechanismus. Er öffnet die Tür für weitergehende Beweise, die bisher unerreichte Sicherheitsgarantien für C++-Programme liefern.
| Zugehörige Institution(en) am KIT | Institut für Programmstrukturen und Datenorganisation (IPD) |
| Publikationstyp | Proceedingsbeitrag |
| Publikationsjahr | 2007 |
| Sprache | Deutsch |
| Identifikator | ISBN: 978-3-88579-199-7 ISSN: 1617-5468 KITopen-ID: 1000017690 |
| Erschienen in | Software Engineering 2007 - Fachtagung des GI-Fachbereichs Softwaretechnik, 27.-30.3.2007, Hamburg. Hrsg.: W.-G. Bleek |
| Verlag | Ges. für Informatik |
| Seiten | 29 - 34 |
| Serie | GI-Edition / Proceedings ; 105 |