%PDF-1.5
%
1 0 obj
<<
/Type /Metadata /Subtype /XML
/Length 9943
>>
stream
Void Safety
Void Safety
Avoiding Null Pointer Dereferencing in an Object-Oriented Language
Alexander Kogtenkov
void safety
null safety
static analysis
object initialization
operational semantics equivalence
Eiffel
certified attachment pattern
object-oriented language safety
source code safety benchmark
big-step operational semantics
formal methods
software modularity
null reference
null pointer dereferencing
Computer science
Software engineering
Formal methods (Computer science)
Software patterns
Object-oriented programming (Computer science)
Object-oriented programming languages
Programming languages (Electronic computers)--Semantics
Source code (Computer science)
Eiffel (Computer program language)
Compilers (Computer programs)
Software Validation
Null pointer dereferencing is a well-known issue in object-oriented programming, and can be avoided by adding special validity rules to the programming language. However, just introducing a single rule is not enough: the whole language infrastructure has to be considered instead. The resulting guarantees are called void safety.
The thesis reviews, in detail, engineering solutions and migration efforts that enabled the transition from classic to void safe code of multiple libraries and projects with lines of code ranging in the millions. Experience with the tiny details of the implementation can be an invaluable source of insight for researcher looking into making a language void safe.
The void safety rules can be divided into three major categories. The first one is the extension of a regular type system with attached (non-null) and detachable (possibly-null) types. Generic programming opens a door to different interpretations. The thesis defines some base void safety properties for formal generic types and specifies void-safety-aware conformance rules.
The second category of rules ensures that newly created objects reach a stable state maintaining the type system guarantees. The thesis proposes two solutions for this object initialization issue and compares them to previous work. It formalizes the rules in the Isabelle/HOL proof assistant and establishes some of their properties. To ensure safety at the end of object life cycle it also specifies validity rules for finalizers. A number of examples are used to demonstrate that the proposed solutions are of practical use and do not suffer from limited expressiveness caused by the lack of additional annotations describing intermediate object states.
The third category of void safety rules covers a practical need to bridge the gap between attached and detachable types. The thesis proposes formal void safety rules for local variables in the context of an object-oriented language that do not require any marks to distinguish between attached and detachable types. It demonstrates advantages of the annotation-free approach with benchmarks based on open source code, discusses implementation decisions and how they are reflected in the formal model.
The thesis concludes with a machine-checkable soundness proof for the rules involving local variables using the Isabelle/HOL proof assistant.
Alexander Kogtenkov
2017-01-31
2017-01-01
2017-01-31
2017-02-27
2017
2017-04-28
Doctoral Thesis
Text
application/pdf
paper-size=A5
321 pages
en
en_US
eng
eng
Copyright (C) 2017 Alexander Kogtenkov
Copyright (C) 2017 Alexander Kogtenkov
http://creativecommons.org/licenses/by-nc-sa/4.0/
Alexander Kogtenkov
Formal methods
Software engineering
Alexander Kogtenkov
Void Safety
Avoiding Null Pointer Dereferencing in an Object-Oriented Language
void safety;null safety;static analysis;object initialization;operational semantics equivalence;Eiffel;certified attachment pattern;object-oriented language safety;source code safety benchmark;big-step operational semantics;formal methods;software modularity;null reference;null pointer dereferencing
D:20170101235959+02'00'
True
This work is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License</a>.
This work is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License</a>.
Dieses Werk ist lizenziert unter einer <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">Creative Commons Namensnennung - Nicht-kommerziell - Weitergabe unter gleichen Bedingungen 4.0 International Lizenz</a>.
Это произведение доступно по <a rel="license" href="http://creativecommons.org/licenses/by-nc-sa/4.0/">лицензии Creative Commons «Attribution-NonCommercial-ShareAlike» («Атрибуция — Некоммерческое использование — На тех же условиях») 4.0 Всемирная</a>.
Alexander Kogtenkov
endstream
endobj
5 0 obj
<<
/Length 843
/Filter /FlateDecode
>>
stream
xmUMo0WxNWH
Z&T~3ڮ zy87?nkNehܤ=77U\;?:v==onU;O^uu#½O
ۍ=٘a?kLy6F/7}̽][H<Sicݾk^90jYVH^v}0<rL
ͯ_/CkBnyWTHkuqö{s\녚"p]ϞќKյu/A )`JbD>`2$`TY'`(ZqBJŌ
)Ǩ%553<,(hlwB60a G+LgıcW crn
q9Mܗ8%CMq.5ShrAI皎\Sȩ]8`Y7ь1Oyezl,dmYĸSSJf-1i:C&e c4R$D&
&+übLaj by+bYBg YJYYr֟bx(rGT̛`F+٭L,C9?d+͊11ӊĊT_~+Cg!o!_??/?㫄Y
?^B\jUP{xᇻL^U}9pQq0O}c}3tȢ}Ə!VOu˷
endstream
endobj
7 0 obj
<<
/Type /ObjStm
/N 100
/First 831
/Length 1645
/Filter /FlateDecode
>>
stream
xڽYM6W[X$m @6!E+ˎzaɻp}
:E,%K̛y3!cg3U2! äPLL)%LO֚Itaf`3c5,k O3[bX0bk*+\-TK3k (0j