CONFIDENT is a toolchain for effective construction and evolution of REST APIs.

HeadREST aims at supporting all phases of RESTful software development supporting: Documentation generation; Code generation (stubs), server and client side; API testing; Runtime monitoring; and
Type checking. Current tools include:

    • HeadRESTLang is a RESTful API specification language, inspired on the Open API Specification, that allows describing behavioural properties of RESTful APIs.
    • TestTool is a tool developed to test RESTful APIs described with HeadREST
    • HR-CodeGen is a tool for generating boilerplate code from HeadREST specifications, taking advantage of the Open API Specification code generation tools

Key ideas:
– Allow detailing the structure of data transferred on the REST interactions
– Use pre and pos-conditions to express (a) the relation between the data sent in the requests and received in the responses and (b) the state changes that occur afterwards

These ideas are then materialized in the HeadREST language, which build on two fundamental concepts:
– refinement types, x:T where e, that consist of x values of type T that satisfy a property e.
– a type predicate, e in T, which returns true or false depending if the value e is or not of type T.

A definition of a type in HeadREST

Representation types help us describe the structure of the data transferred. The supported representation types are: objects, arrays, refinement types, scalar types (including integer, boolean, string and URITemplate) and any as our top type.

A specification of an operation in HeadREST


Nuno Burnay



HeadREST Eclipse plugin
Update Site
Installing the Z3 binaries
        • Download the correct zip binaries for your Operative System.
        • Extract the archive and add the Z3 bin folder to your system path.
          • Unix: LD_LIBRARY_PATH environment variable
          • MAC OS X: Add a symbolic to libz3.dylib from folder /usr/local/lib; add a symbolic link libz3java.dylib from folder /Library/Java/Extensions
        • Or clone the new Z3 repository and follow the instructions to compile it.
        • Add the generated folder to the system path.
Installing the Eclipse HeadREST Plugin
        • Go to the Help menu → Install New Software…
        • Type in in the work with field and press Enter;
        • Select Xtext → Xtext Complete SDK (confirm it is at least v2.13.0);
        • Restart Eclipse;
        • Go to the Help menu → Install New Software…
        • Type in in the work with field and press Enter;
        • Select HeadREST;
        • 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 HeadREST project
        • In Eclipse go to File->New…->Project. Create a new Java Project;
        • Create a .rspec file;
        • If asked, confirm to convert to a Xtext project;
        • Write your specification in the created .rspec file. Here you can find some examples.
        • Right click inside the editor and choose Validate (first option with this name in the menu);
        • Wait until Eclipse reports no more tasks in progress.

HeadREST terminal version

LD_LIBRARY_PATH=<path to folder with the libraries of Z3> java -jar headrest.jar <path to .rspec file>


Learning HeadREST

Head over to the Online tutorial to learn and practice using HeadREST with no installation on your machine.


      • F. Ferreira, T. Santos, F. Martins, A. Lopes and V. Vasconcelos. Especificação de Interfaces Aplicacionais REST. In Actas do 9º Encontro Nacional de Informática, INFORUM 2017. pdf
      • Fábio Ferreira , Automatic Test Generation for RESTful APIs , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2017.  pdf
      • Vasco T. Vasconcelos, Antónia Lopes, and Francisco Martins, HeadREST: A Specification Language for RESTful APIs, 24th International Conference on Types for Proofs and Programs. pdf