Dynamic Interfaces
Vasco T. Vasconcelos, Simon J. Gay, Antonio Ravara,
Nils Gesbert, and Alexandre Z. Caldeira
Abstract
We define a small class-based object-oriented language in which the
availability of methods depends on an object’s abstract state: objects’
interfaces are dynamic. Each class has a session type which provides a
global specification of the availability of methods in each state. A
key feature is that the abstract state of an object may depend on the
result of a method whose return type is an enumeration. Static typing
guarantees that methods are only called when they are available. We
present both a type system, in which the typing of a method specifies
pre- and post-conditions for its object’s state, and a typechecking
algorithm, which infers the pre- and post-conditions from the session
type, and prove type safety results. Inheritance is included; a
subtyping relation on session types, related to that found in previous
literature, characterizes the relationship between method availability
in a subclass and in its superclass. We illustrate the language and its
type system with example based on a Java-style iterator and a hierarchy
of classes for accessing files, and conclude by outlining several ways
in which our theory can be extended towards more practical languages.
Presented at FOOL'09; Saturday, 24 January
2009, Savannah, Georgia, USA.