On an algorithm determining direct superclasses in Java and similar languages with inner classes—Its correctness, completeness and uniqueness of solutions

Some object oriented programming languages allow inner classes. All of them admit inheritance. This combination of inner classes and inheritance is very fruitful however less known. On the other hand it creates a serious problem: how to determine the direct superclass of a given class C, i.e. the class which class C directly inherits from. For there may be several classes of the same name in one program. A specification of the problem and a non-deterministic algorithm are provided. We prove that the algorithm is correct w.r.t. the specification and complete, i.e. if the algorithm signals an error then no solution exists. We show that the specification itself has at most one solution, in other words, it is a complete specification. This proves also that the corresponding parts of Java Language Specification are consistent and define uniquely a fragment of Java semantics.