Formal methods for components and objects

Universe types characterise aliasing in object oriented programming languages and are used to reason modularly about programs. In this report we formalise prior work by M ̈uller and Poetzsch-Heffter, who designed the Universe Type System for a core subset of Java. We present our work in two steps. We first give a Topological Universe Type System and show subject reduction to a small-step dynamic semantics for our language. Motivated by concerns of Modular verification, we then give an Encapsulation Universe Type System (based on the owner-as-modifier principle), prove subject reduction with respect to the former small-step semantics, and show how the type system can be used for modular verification.peer-reviewe