We define a small functional calculus that expresses class-based object oriented features and is modelled on the similar calculi of Featherweight Java [Igarashi, Pierce, and Wadler '99} and Middleweight Java [Bierman, Parkinson, and Pitts '03], which are ultimately based upon the Java programming language. We define a predicate system, similar to the one defined in [vanBakel and de'Liguoro '08], and show subject reduction and expansion, and argue that program analysis systems can be built on top of this system. Generalising the concept of approximant from the Lambda Calculus, we show that all expressions that we can assign a predicate to have an approximant that satisfies the same predicate. From this, a characterisation of (head-)normalisation follows.
