Proceedings of ISP RAS


Mechanically Proved Practical Local Null Safety

A.V. Kogtenkov (ETH, Zürich, Switzerland)

Abstract

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.

Keywords

null safety, void safety, static analysis, Eiffel, formal methods, big-step operational semantics, preservation theorem, operational semantics equivalence

Edition

Proceedings of the Institute for System Programming, vol. 28, issue 5, 2016, pp. 27-54.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(5)-2

Full text of the paper in pdf Back to the contents of the volume