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) for server- and client-side; API testing; Runtime monitoring; and Type checking. Current tools include:

    • HeadREST is a specification language of RESTful APIs, inspired on Open API Specification, but that goes beyond the description of the structure of the data exchanged and allows also to correlate I/O and I/O with server state.
    • HeadREST-TestTool is a tool developed to test RESTful APIs described with HeadREST.
    • HeadREST-CodeGen is a tool for generating client- and server-side code from HeadREST specifications, taking advantage of the Open API Specification code generation tools.
    • SafeRestScript is a client-side language that statically validates REST calls against a HeadREST specification.

HeadREST  Key ideas:
– Use types to express properties of states and of data exchanged in REST interactions
– Use pre and post-conditions to express the relationship between data in requests and responses as well as resource state changes

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

Team

Vasco T. Vasconcelos
Francisco Martins
Project

Downloads

HeadREST Eclipse plugin
Update Site
http://download.rss.di.fc.ul.pt/confident/HeadREST/update-site/
Requirements
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
Creating a HeadREST project
    • In Eclipse go to File->New…->Project. Create a new Java Project;
    • Create a .hrest file;
    • If asked, confirm to convert to a Xtext project;
    • Write your specification in the created .hrest file (some examples);
    • Safe the file;
    • 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 .hrest file>

SafeRestScript Eclipse plugin
Update Site
http://download.rss.di.fc.ul.pt/confident/SafeRestScript/update-site/
Requirements
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
Installing Boogie
    • Clone Boogie repository.
    • Build Boogie according with the project README.
    • Add the binnaries folder of Boogie to system path.
    • Link Boogie to Z3 binaries:
      • Windows: (run as admin) mklink /H <path to Boogie>\Binaries\z3.exe <path to Z3>\bin\z3.exe
      • Unix: ln -s <path to Z3>/bin/z3 <path to Boogie>/Binaries/z3.exe
Installing the Eclipse SafeRestScript Plugin
    • Install SafeRestScript plugin:
      • Go to the Help menu → Install New Software…
      • Type in http://download.rss.di.fc.ul.pt/confident/SafeRestScript/update-site/ in the work with field and press Enter;
      • Select SafeRestScript and 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.
      • Create a SafeRestScript project:
        • In Eclipse go to File → New… → Project. Create a new SafeRestScriptProject;
          • Select the project name and location. Press Next;
          • Select the Default template. Press Next;
          • If you are in an Unix OS:
            • Select the checkbox Generate configuration file;
            • After the project is created, complete the srs.config file as describe in this.
        • Create a .srs file;
        • Save the file to validate the program:
          • Wait until Eclipse reports no more tasks in progress;
          • If the validation succeed the JavaScript file generated will be in the src-gen folder.
SafeRestScript terminal version

Download from http://download.rss.di.fc.ul.pt/confident/SafeRestScript/srs.jar the terminal version of SafeRestScript.

java -jar srs.jar <path to .srs file>

HeadREST-Codegen
CodeGen Overview
Examples

Examples of Client SDKs and server stubs generated by HeadREST-Codegen from HeadREST specifications

 

Learning HeadREST

Go to the Online tutorial to learn how to specify REST APIs with HeadREST with no installation required.

Publications

  • 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
  • Telmo Santos, Code Generation for RESTful APIs in HEADREST, MSc Thesis, Departamento de Informática, FCUL, DI/FCUL, July 2018. pdf
  • Vasco T. Vasconcelos, Francisco Martins, Antónia Lopes, Nuno Burnay. HeadREST: A Specification Language for RESTful APIs, In Models, Languages, and Tools for Concurrent and Distributed Programming. pdf
  • Nuno Burnay, Antónia Lopes, Vasco T. Vasconcelos. Safe(REST)Script, In Actas do 11º Encontro Nacional de Informática, INFORUM 2019. pdf
  • Nuno Burnay, Types to the Rescue: Verification of REST APIs Consumer Code, MSc Thesis, Departamento de Informática, FCUL , DI/FCUL, 2019. pdf