Formalisation and implementation of an algorithm for bytecode verification of @NonNull types