KIT | KIT-Bibliothek | Impressum | Datenschutz

C++ ist typsicher? Garantiert!

Wasserrab, Daniel; Nipkow, Tobias; Snelting, Gregor; Tip, Frank

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.


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 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, Bonn
Seiten 29 - 34
Serie GI-Edition / Proceedings ; 105
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page