Reasoning about objects using process calculus techniques

This thesis investigates the applicability of techniques known from the world of process calculi to reason about properties of object-oriented programs. The investigation is performed upon a small object-oriented language - The Sigma-calculus of Abadi and Cardelli. The investigation is twofold: We investigate translations of Sigma-calculi into process calculi, with the idea that one should be able to show properties of Sigma-calculus program by showing properties about their translation. We present translations of two Sigma-calculi into Pi-calculi. A translation of the untyped functional Sigma-calculus turns out to be insufficient. Based on our experiences, we present a translation of a typed imperative Sigma-calculus, which looks promising. We are able to provide simple proofs of the equivalence of different Sigma-calculus objects using this translation. We use a labelled transition system adapted to the Sigma-calculus to investigate the use of process calculi techniques directly on the Sigma-calculus. The results obtained are of a fairly theoretical nature. We investigate the connection between the operational and denotaional semantics for a typed functional Sigma-calculus. The result is that Abadi and Cardelli's denotational model is sound but not complete with respect to the operational semantics. We also construct a modal logic for the typed functional Sigma-calculus, provide a translation of types to a sub-logic and prove the translation is sound and complete. The amount work required to perform these investigations indicate, that although it is perfectly possible to use process calculus techniques on object oriented languages, such techniques will not come to widespread use, but only be limited to reasoning about critical parts of a language or program design.