This implementation is based on the OOPSLA 2003 paper
Declaring and Checking Non-null Types in an Object-Oriented Language
by Manuel Fähndrich and K.Rustan M. Leino