Gesellschaft für Informatik e.V.

Lecture Notes in Informatics


Software Engineering 2007, Fachtagung des GI-Fachbereichs Softwaretechnik 27. - 30.03.2007 in Hamburg P-105, 29-34 (2007).


2007


Editors

Stefan Böttinger (ed.), Ludwig Theuvsen (ed.), Susanne Rank (ed.), Marlies Morgenstern (ed.)


Contents

C++ ist typsicher? Garantiert!

Daniel Wasserrab , Tobias Nipkow , Gregor Snelting and Frank Tip

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.


Full Text: PDF

ISBN 978-3-88579-195-9


Last changed 04.10.2013 18:13:43