Dependent Object-oriented Language, or DOL for short, is an object-oriented language featuring mutable objects and dependent types that supports class-based inheritance with subtyping.

While rooted in techniques formulated for dependently-typed functional languages, DOL's type system is able to capture more than just value properties and pure computations. Using a combination of index refinements and method type signatures inspired on Hoare-style pre- and postconditions, it gives programmers the ability to reason about effectful computations.

This is (as far as we know) the first implementation of a type system combining three very different features: dependent types, mutable objects, and inheritance with subtyping. With the assistance of an external SMT solver, the tool can verify certain program invariants at compile time, including the binary search tree property.