Semantic Predicate Types and Approximation for Class-based Object Oriented Programming

TL;DR

This paper extends Featherweight Java with a predicate system based on intersection types, providing a semantic foundation for class-based object-oriented programming and demonstrating approximation properties.

Contribution

It introduces a sound, expressive predicate system for Featherweight Java, generalizes the concept of approximants, and links predicates with class-specific predicate languages.

Findings

The predicate system is sound and expressive.

All expressions with assigned predicates have approximants satisfying the same predicates.

The approach generalizes the concept of approximant from Lambda Calculus.

Abstract

We apply the principles of the intersection type discipline to the study of class-based object oriented programs and; our work follows from a similar approach (in the context of Abadi and Cardelli's Varsigma-object calculus) taken by van Bakel and de'Liguoro. We define an extension of Featherweight Java, FJc and present a predicate system which we show to be sound and expressive. We also show that our system provides a semantic underpinning for the object oriented paradigm by generalising the concept of approximant from the Lambda Calculus and demonstrating an approximation result: all expressions to which we can assign a predicate have an approximant that satisfies the same predicate. Crucial to this result is the notion of predicate language, which associates a family of predicates with a class.