A Virtual Class Calculus

Abstract

Virtual classes are class-valued attributes of objects.
Like virtual methods, virtual classes are defined in
an object’s class and may be redefined within subclasses.
They resemble inner classes, which are also
defined within a class, but virtual classes are accessed
through object instances, not as static components
of a class. When used as types, virtual classes depend
upon object identity – each object instance introduces
a new family of virtual class types. Virtual classes support large-scale program composition techniques,
including higher-order hierarchies and family
polymorphism. The original definition of virtual
classes in Beta left open the question of static type
safety, since some type errors were not caught until
runtime. Later the languages Caesar and gbeta have
used a more strict static analysis in order to ensure
static type safety. However, the existence of a sound,
statically typed model for virtual classes has been a
long-standing open question. This technical report
presents a virtual class calculus, vc, that captures
the essence of virtual classes in these full-fledged programming languages. The key contributions of the
paper are a formalization of the dynamic and static
semantics of vc and a proof of the soundness of vc.
Categories: D.3.3 [Language Constructs and Features]:
Classes and objects, inheritance, polymorphism.
F.3.3 [Studies of Program Constructs]:
Object-oriented constructs, type structure. F.3.2
[Semantics of Programming Languages]: Operational
semantics.