Mechanically Proved Practical Local Null Safety

• Published in: Труды Института системного программирования РАН
• Main Author: A. V. Kogtenkov
• Format: Article
• Language: English
• Published: Russian Academy of Sciences, Ivannikov Institute for System Programming 2018-10-01
• Subjects: безопасность пустых указателей; статический анализ; eiffel; формальные методы; крупношаговая операционная семантика; теорема о сохранении; эквивалентность операционных семантик
• Online Access: https://ispranproceedings.elpub.ru/jour/article/view/168
• ISSN: 2079-8156; 2220-6426

Null pointer dereferencing is a well-known bug in object-oriented programs. It can be avoided by adding special validity rules to a language in which programs are written. Are the rules sufficient to ensure absence of such exceptions? This work focuses on null safety for intra-procedural context where no additional type annotations are needed and formalizes the rules in Isabelle/HOL proof assistant. It then proves null-safety preservation theorem for big-step semantics in a computer-checkable way. Finally, it demonstrates that with such rules null-safe and null-unsafe semantics are equivalent.