Dependent Object-oriented Language

DOL is a Dependent Object-oriented Language featuring dependent types, mutable objects and class-based inheritance with subtyping.

 

The language brings classes and dependent types into play so as to enable types (classes) to be refined by value parameters (indices) drawn from a restricted constraint domain. This combination allows statically checking interesting properties of imperative programs that are impossible to check in traditional static type systems for objects.

DOL is therefore an attempt to provide a middle ground between simple invariants enforced by traditional type systems and more expressive (and complex) ones supported by verification techniques.

The DOL compiler is responsible for typechecking DOL programs, relying on the Z3 SMT solver for checking the constraints issued by types, and for translating DOL source code into pretty-printed Java classes. It supports Eclipse IDE integration with syntax colouring, code completion, on-the-fly error checking, and other conveniences.

Team

Joana Campos
Vasco T. Vasconcelos

Downloads

DOL Eclipse plugin

Update Site
http://download.rss.di.fc.ul.pt/dol/update-site
Requirements
        • Eclipse IDE installed (it seems to be working with Eclipse Oxygen.2 and Java 8).
Installing the Z3 binaries
        • Download the correct zip binaries for your Operative System (check the planed releases).
        • Extract the archive and add the Z3 bin folder to your system path.
        • Or clone the new Z3 repository and follow the instructions to compile it.
        • Add the generated folder to the system path.
Installing the Eclipse DOL Plugin
        • Go to Help → Install New Software…
        • Type in http://download.eclipse.org/modeling/tmf/xtext/updates/composite/releases/ in the work with field and press Enter;
        • Install the feature Xtext Complete SDK;
        • Restart Eclipse;
        • Go to Help → Install New Software…
        • Type in the URL for DOL update site in the work with field and press Enter;
        • Select the Dol SDK Feature;
        • Press the Next button;
        • It takes a while for the update site to resolve the dependencies and contact the necessary update sites;
        • Trust us and accept the unsigned plugin;
        • Restart Eclipse. The installation is now complete.
Creating a DOL project
        • In Eclipse go to File->New->Java Project. Create a new Java Project;
        • Inside this project create a new file; the name of the file is not important, but the file extension must be dol;
        • As soon as the file is created, you will be asked to add the Xtext nature to your project. You should accept that;
        • Write your program in the created .dol file. Here you can find some examples;
        • Notice that a src-gen folder is automatically created as soon as you save the file. At this point, you should also add this generated folder to the project’s source folders by going to Build Path → Use as Source Folder.
DOL language library

In order to use library classes like Top, Integer and Boolean, you have to add them as dependencies to your project. Download DOL’s library to a local folder, then add it by going to Java Build Path → Libraries → Add External Class Folder.

DOL Artifact

Another option is to use a virtual machine containing the plugin and examples already setup in an Eclipse distribution:

Try DOL

Head over to the online tutorial to learn and practice DOL with no installation on your machine.

Publications

      • Joana Campos and Vasco T. Vasconcelos, Dependent Types for Class-based Mutable Objects, ECOOP, 13:1–13:28, 2018, 10.4230/LIPIcs.ECOOP.2018.13
      • Joana Campos, Adding Dependent Types to Class-based Mutable Objects, PhD Thesis, Universidade de Lisboa, 2018 (PDF)
      • Joana Campos and Vasco T. Vasconcelos, Programming with mutable objects and dependent types, Atas do Oitavo Simpósio de Informática, INForum 2016 (PDF)
      • Joana Campos and Vasco T. Vasconcelos, Imperative objects with dependent types, Formal Techniques for Java-like Programs (FTfJP 2015), 2:1–2:6, 2015 (PDF)