Mechanically Proved Practical Local Null Safety
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.
Proceedings of the Institute for System Programming, vol. 28, issue 5, 2016, pp. 27-54.
ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).