Laddar…
Academic Journal
Mechanically Proved Practical Local Null Safety
A. V. Kogtenkov
Труды Института системного программирования РАН, Vol 28, Iss 5, Pp 27-54 (2018)
Sparad:
| Titel | Mechanically Proved Practical Local Null Safety |
|---|---|
| Författarna | A. V. Kogtenkov |
| Utgivningsår |
2018
|
| Källa |
Труды Института системного программирования РАН, Vol 28, Iss 5, Pp 27-54 (2018)
|
| Beskrivning |
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.
|
| Dokumenttyp |
article
|
| Språk |
English
Russian |
| Information om utgivare |
Ivannikov Institute for System Programming of the Russian Academy of Sciences, 2018.
|
| Ämnestermer | |
