Abstract

The primary problem with structural subtyping, semantic malformance (e.g. contract violations), can be alleviated by introducing behavioral constraints into the specification of the subtype. This paper describes a mechanism to implement implicit behavioral subtyping, by applying structural subtyping as well as precondition and postcondition assertions to traits.

Introduction

This work is demonstrated using the Heron programming language. Heron is a statically typed experimental programming language, which is implemented using a Heron to C++ translator, HeronFront. The HeronFront tool translates trait constructs written in Heron to classes with the implicit behavioral subtyping semantics described in this paper. Apart from the introduction of traits and some rather minor syntactic difference, the Heron langauge shares C++ syntax and semantics.

Traits

Traits were first described by Schärli et al. [Sch03] as a compositional model for structuring object oriented programs. A trait is a construct similar to Java interfaces in that it is used to characterize the function signatures (sometime described as a method dictionary) for a set of types, and can be used as a polymorphic reference which binds to a conforming object. The Heron trait has similar syntax to traits in Scala 1.0 [Ode05] which has since been replaced by mixin-classes. The function signatures that it provides are known as the required functions, and are sometimes referred to as "super-sends" because they delegate the implementation to the super type. Unlike a Java interface, a trait may also have member functions which call other member functions or one of the required functions. The member functions of a trait are referred to as extension functions to clearly delineate them from class member functions.

Structural Subtyping

Structural subtyping (also known as implicit subtyping, signature based polymorphism, and colloquially as duck-typing), is a method of deducing a subtype relationship at either run-time or compile-time. Trait instances in Heron are associated with super types using a structural subtyping mechanism.

Implicit subtyping has several advantages:

• separation of mechanisms of inheritance and subtyping - the problems with this are explored in depth with regards to the C++ language by Baumgartner and Russo [Bau95].
• subtyping without recompilation - new subtype relationships can be created without requiring recompilation or rewriting of the super-type. This not only increases compilation times significantly, it makes binary-only distribution of components more feasable and useful, and cross-language development more feasable.
• more flexible and extensible designs - all possible subtype relationships don't have to be decided a priori, and can be restricted in scope to particular modules.
• mock objects - it is easier to create mock objects for testing, a crucial component of TDD methodologies

Implicit subtyping can be achieved, rather surprisingly, in the C++ programming language using only template meta-programming techniques [Dig04], and more conveniently with macros [Tur05].

Several dynamically typed languages support structural subtyping but only a few statically typed language provide support for it. The main languages being the various ML dialects. A now discontinued extension to the GCC C++ compiler, did support a similar structure also called signatures [Bau97].

Heron Syntax

Except where stated, Heron statements have precisely the same syntax and semantics as C++. HeronFront does a literal mapping of most statements from Heron to C++ with no checking.

Heron traits are divided up into four sections (inherits, requires, public, private), and optional template parameters. Heron also introduces two new keywords: _result and _override.

The _result keyword corresponds to a variable which is implicitly declared at the beginning of every non-void function in a trait. Every non-void function in a trait also contains the implicit statement "return _result;" as a last line. A return statement takes on a new meaning in Heron, it assigns the expression to _result, and then jumps to the end of the function, so that the postconditions can still be evaluated.

The _override keyword corresponds to a delegation of the current function to the appropriate function in the super-type. This means that a required function in a trait with no preconditions and posconditions can be written equivalently either as:

1)

  trait T {
    requires {
      def f() : int;
    }
  }

2)

  trait T {
    requires {
      def f() : int {
        _override;
      }
    }
  }

The actual C++ code generated for the _override keyword would resemble more or less:

  _result = _get()->f();

The _get() reserved member function returns a pointer to a class which forwards the function to the bound object.

Trait Semantics

An instance of a trait in Heron can bound to any concrete object which provides the appropriate function signatures, for example:

  /*
    Heron code which we assume is translated into a C++
    header file using HeronFront and #included

    trait MyTrait {
      require {
        def set(int n);
        def get() : int;
      }
    }
  */

  class MyClass {
    public:
      MyClass() : m(0) { }
      void set(int n) {
        data = n;
      }
      int get() {
        return data;
      }
    private:
      int data;
  };

  int main() {
    MyTrait t;
    MyClass c;
    t = c;
    printf("%d\n", t.get()); // outputs 0
    printf("%d\n", c.get()); // outputs 0
    t.set(1);
    printf("%d\n", t.get()); // outputs 1
    printf("%d\n", c.get()); // outputs 1
  }

Heron Trait Grammar

  statement ::==
    any legal C++ statement

  function-param ::==
    type identifier

  function-return-type ::==
    : type

  function ::==
    def identifier ( function-param* ) function-return-type?
    { statement* }

  function-or-type-or-macro ::==
    function | class | trait | macro

  template-parameters ::==
    [ meta-type identifier ]

  inherits-section ::==
    inherits { type-specifier* }

  requires-section ::==
    requires { function* }

  public-section ::==
    public { function-or-type-or-macro* }

  private-section ::==
    private { function-or-type-or-macro* }

  trait ::==
    trait identifer template-parameters? {
    inherits-section?
    requires-section?
    public-section?
    private-section?
    }

Same Structure, Different Semantics

Implicit subtyping has the disadvantage that syntactic conformance can occur in types which do not share semantics. An illustrative example can be found when comparing LIFO stacks and FIFO stacks. This is illustrated in Example X.

Example

  trait Stack[T : type] {
    requires {
      def push(T x);
      def pop();
      def top() : T&;
      def is_empty() : bool;
    }
  }

  trait FifoStack[T : type] {
    inherits {
      Stack[T];
    }
  }

  trait LifoStack[T : type] {
    inherits {
      Stack[T];
    }
  }

The problem occurs when we try to execute some algorithm which expects a FifoStack, but instead receives a LifoStack.

The proposed solution to the problem of structural conformance with semantic malformance, is to introduce contract verification, in the form of precondition and postcondition assertions. In other words implicit behavioral subtyping.

Contract Verification

A contract is the name collectively given to the preconditions, postconditions, and invariants, which a type is expected to satisfy. A contract can be used to characterize the behavior of a type [Mey97], [Lis99]. Rather than creating a brand new syntax, including keywords, Heron relies solely on the C++ language facilities to enable the programmer to define how they choose to verify the preconditions and postconditions.

Contract verification can be achieved by writing the required function using the explicit syntax and the _override keyword, and inserting precondition and postcondition checks before and after respectiviely the _override call, as follows:

How the pre and post functions are implemented is up to the programmer, but they can be implemented as macros create two new macros as follows:

  #define pre(expr) assert(expr && "precondition violation")
  #define post(expr) assert(expr && "postcondition violation")

Implicit Behavioral Subtyping

Implicit behavioral subtyping is a stronger form of structural subtyping which introduces precondition and postcondition assertions into the verification. The following example shows the differentiation between a FIFO stack and LIFO stack

  trait Stack[T : type] {
    requires {
      def push(T x);
      def pop();
      def top() : T&;
      def is_empty() : bool;
    }
  }

  trait FifoStack[T : type] {
    inherits {
      Stack[T];
    }
    requires {
      def push(T x) {
        if (!is_empty()) {
          T old = top();
          _override;
          post(old == top());
          post(!is_empty());
        }
        else {
          _override;
          post(!is_empty());
        }
      }
      def pop() {
        pre(!is_empty());
        _override;
      }
      def top() : T& {
        pre(!is_empty());
        _override;
      }
    }
  }

  trait LifoStack[T : type] {
    inherits {
      Stack[T];
    }
    requires {
      def push(T x) {
        _override;
        post(!is_empty());
        post(x == top());
      }
      def pop() {
        pre(!is_empty());
        _override;
      }
      def top() : T& {
        pre(!is_empty());
        _override;
      }
    }
  }

The difference in behavior between the two kinds of stack ADT's, can be expressed as whether or not push affects the status of the top, in the case of a non-empty stack. This is a non-trivial assertion, and to express it we need the full the range of the language. To achieve this, Heron allows any C++ statement to be used before or after the super-send (i.e. the _override keyword).

Verifying Invariants

Heron currently provides no convenient syntax for verifying invariants, however this should change in the next major release of HeronFront. See the section "Future Direction" for more information. For the time being an invariant can be simply explicitly checked after each required function along with the postconditions.

External Function Dispatch versus Virtual Function

Common OOPL implementations implement runtime polymorphism using the mechanism of virtual functions. One difference with Heron is that it implements runtime function dispatch externally to the class, rather than through the use of virtual function. This means that a pointer to a function dispatch table is associated with the trait instance rather than the object instance. This approach carries several advantages

• intra-method calls can be more easily inlined
• the memory and cpu overhead associated with polymorphism only occurs when the polymorphism is needed rather than throughout the lifetime of every single object.
• no more undiscovered bugs due to unanticipated virtual function overrides - testing of OO designs frequently overlooks the various possibilities of virtual function override abuse.

The Generated C++ Code

HeronFront generates C++ classes which support signature matching semantics. This is accomplished using template meta-programming techniques. Every trait is associated with a single class which has a template constructor, a template assignment operator, and a dispatcher object along with the expected required and extension functions. The dispatcher object is implemented as a concrete subtype inheriting from an abstract supertype which contains a pure virtual function for each required function in the trait. The extension functions are implemented directly in the trait class. Example X contains an example of code generated for a simple trait.

  trait Indexable[type Element] {
    requires {
      def get(uint n) : Element {
        assert(n < count());
        _override;
      }
      def set(uint n, Element x) {
        assert(n < count());
        _override;
      }
      def count() : uint;
    }
    public {
      def is_empty() {
        return count() == 0;
      }
    }
  }

Here is the code generated by the most recent version of HeronFront:

  template<class Element >
  struct Indexable {
    template<typename _T>
    Indexable(_T& _x) {
      new(&_data) _concrete<_T>(&_x);
      assert(sizeof(_concrete<_T>) <= (sizeof(void*) * 2));
      }
    struct _abstract {
      virtual Element get(uint n) = 0;
      virtual void set(uint n, Element x) = 0;
      virtual uint count() = 0;
      };
    template<typename _T>
    struct _concrete : _abstract {
      _concrete(_T* x) : _object(x) { }
      Element get(uint n) {
        Element _result;
        #define _override return _object->get(n)
        assert ( n < count ( ) ) ;
        _override ;
        return _result;
        #undef _override
        }
      void set(uint n, Element x) {
        #define _override _object->set(n, x)
        assert ( n < count ( ) ) ;
        _override ;
        #undef _override
        }
      uint count() {
        return _object->count();
        }
      _T* _object;
      };
    _abstract* _get() { return reinterpret_cast<_abstract*>(_data); }
    _abstract* operator->() { return _get(); }
    void* _data[2];
    // requires section functions
    Element get(uint n) {
      return _get()->get(n);
      }
    void set(uint n, Element x) {
      _get()->set(n, x);
      }
    uint count() {
      return _get()->count();
      }
    // public non-delegated member functions
    bool is_empty() {
      bool _result;
      return count ( ) = 0 ;
      return _result;
      }
    };

This code is quite complex, but the most important characteristics are:

• it has the same memory footprint as two void pointers
• it uses the C++ virtual function dispatch mechanism internally to dynamically dispatch functions rather than the more unweildy function pointer table approach first described in [Dig04].
• it uses placement new to construct the correct data type internally

Future Directions

The largest gap in this work is the inability to express a class invariant in a single location. Class invariants currently have to be verified with the preconditions and postconditions (arguably either one is sufficient). A class invariant is an example of a crosscutting concern. Direct support for class invariant verification can be added to a programming language such as Java or C++ with relative ease, but this ignores the more general problem of the inability to express crosscutting concerns. Ideally a language would provide such a mechanism which can then be used to implement invariant verification, along with other crosscutting concerns.

It is the author's desire to introduce an extremely minimal form of aspect oriented programming support [Kic97] into Heron in the form of macros which are automatically inserted around each member function. These macros would be ideally associated with a class, or a module, and can be inherited from one class to another.

There is a possibility of introducing a mutable state into traits in the context of Heron.

Acknowledgements

Special thanks to Peter Grogono. Thanks also to the many people at Artima.com who have patiently discussed the topics of structual and behavioral subtyping with me.

References

• [Lis99] Behavioral Subtyping Using Invariants and Constraints, July 1999, Barabara H Liskov, Jeanette M Wing, CMU-CS-99-156
• [Mey97] B. Meyer. Object-Oriented Software Construction, Second Edition. Prentice Hall, 1997.
• [Bau95] Signatures: A Language Extension for Improving Type Abstraction and Subtype Polymorphism in C++ (1995) Gerald Baumgartner, Vincent F. Russo Software--Practice \& Experience
• [Bau97] Implementing signatures for C++, Gerald Baumgartner, Vincent F. Russo, ACM Transactions on Programming Languages and Systems (TOPLAS) archive volume 19, Issue 1 (January 1997) Pages: 153 - 187
• [Fin01] http://www.ccs.neu.edu/scheme/pubs/fse01-flf.pdf Behavioral Contracts and Behavioral Subtyping, FSE 2001, Robert Bruce Findler, Mario Latendresse, Matthias Felleisen
• [Kic97] Kiczales, Gregor, John Lamping, Anurag Mendhekar, Chris Maeda, Cristina Lopes, Jean-Marc Loingtier, and John Irwin (1997). "Aspect-Oriented Programming" Proceedings of the European Conference on Object-Oriented Programming, vol.1241, pp.220–242.
• [Sch03] Traits: Composable Units of Behavior, Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P. Black. University of Berne / OGI School of Science & Engineering, May 2003 Proceedings of ECOOP 2003
• [Dig04] C++ with Interfaces, Christopher Diggins, September 2004 C++ Users Journal
• [Tur05] http://www.kangaroologic.com/interfaces/
• http://research.microsoft.com/specsharp/
• [Ode05] http://scala.epfl.ch/docu/files/ScalaReference.pdfScala Language Specification, June 20, 2005

class CA {
  public {
    def a();
  }
}

trait Renamer {
  requires {
    a();
  }
  public {
    b() {
      a();
    }
  }
}

trait TB {
  requires {
    b();
  }
}

def main() {
  CA a;
  TB b = Renamer(a);
}

class L1 {
  public {
    class M1 {
      public {
        def f1();
      }
    }
    trait T1 {
      requires {
        def f1();
      }
    }
  }
  def multiply(T1 x, T1 y) {
    ...
  }
}

class L2 {
  public {
    class M2 {
      public {
        def f2();
      }
    }
    trait T2 {
      requires {
        def f2();
      }
    }
  }
  def multiply(T1 x, T1 y) {
    ...
  }
}


class L3 {
  public {
    trait T2toT1 {
      requires {
        def f2();
      }
      public {
        def f1() {
          f2();
        }
      }
    }
    def multiply(T1 x, T2 y) {
      L1 z;
      z.multiply(x, T2toT1(y));
    }
  }
}