|
This article is cited in 2 scientific papers (total in 2 papers)
Mechanically proved practical local null safety
A. V. Kogtenkov ETH Zürich
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.
Citation:
A. V. Kogtenkov, “Mechanically proved practical local null safety”, Proceedings of ISP RAS, 28:5 (2016), 27–54
Linking options:
https://www.mathnet.ru/eng/tisp66 https://www.mathnet.ru/eng/tisp/v28/i5/p27
|
Statistics & downloads: |
Abstract page: | 131 | Full-text PDF : | 142 | References: | 32 |
|