Confident

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

 

CONFIDENT aims at supporting all phases of RESTful software development with:

  • Documentation generation;
  • Code generation (stubs) for server- and client-side;
  • API testing;
  • Runtime monitoring;
  • Type checking.

HeadREST: an IDL for RESTful APIs

CONFIDENT is developed around HeadREST, a interface description language for RESTful APIs, inspired on Open API Specification (OAS), but that goes beyond the description of the structure of the data exchanged and allows to correlate I/O and I/O with server state.

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

The type system builds 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.

Definition of two representation types in HeadREST useful to describe Instagram RESTful API.

Representation types help us to describe the structure of the data transferred in the requests and responses. These types can be objects, arrays, refinement types, scalar types (including integer, boolean, string and URITemplate) and any (the top type).

Triples of the form {pre} m u {pos}, where m is an operation and u is a URI template, allow us to specify the behaviour of the API endpoints.

Specification of an endpoint of Instagram RESTful API.

Learn more about HeadREST.  In this online tutorial you can learn more about how to specify REST APIs with HeadREST and try the HeadREST validator (no installation is required).

SafeRESTScript: a type-safe language

SafeRESTScript (SRS for short) is a type-safe subset of JavaScript equipped with primitives to natively support REST calls. These calls are statically validated against HeadREST specifications of the corresponding endpoints.

A SafeRESTScript program consuming an endpoint of Instagram RESTful API; the type checker spots an error in the use of the response data.

Learn more about SafeRESTScript.  In this paper you can learn more about SRS and its type checker.

Tools

Several tools are currently available:

    • HeadREST-Validator is a tool that validates wellformedness of HeadREST specifications. The tool is publicly available as a Eclipse plugin and a jar.
    • SafeRestScript-Compiler is a tool that statically analyses SRS programs that consume RESTful APIs specified in HeadREST. The tool transpiles valid programs into JavaScript and is publicly available as a Eclipse plugin and a jar.
    • HeadREST-TestTool is a tool developed to test RESTful APIs described with HeadREST specifications.
    • HeadREST-CodeGen is a tool for generating client- and server-side code from HeadREST specifications.

Learn more about these tools below.  

Team

Vasco T. Vasconcelos
Francisco Martins

Project

Tools & Downloads

HeadREST Eclipse plugin

This is an Eclipse plugin with an editor and validator for HeadREST specifications.

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);
    • Save the file;
    • Wait until Eclipse reports no more tasks in progress.

HeadREST terminal version

HeadREST validator is also available as a jar.

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

SafeRestScript Eclipse plugin

This is an Eclipse plugin with an editor and compiler for SafeRESTScript programs.

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

This tool generates server and client code from HeadREST specifications. The tool capitalizes on Swagger Codegen for OAS extending it in order to take into account what that can be expressed in HeadREST specs.

Overview
Examples

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

Publications

  • Nuno Burnay, Antónia Lopes, Vasco T. Vasconcelos. Statically Checking REST API Consumers, In Software Engineering and Formal Methods, SEFM 2020. pdf (examples, extended version, presentation)
  • Nuno Burnay, Types to the Rescue: Verification of REST APIs Consumer Code, MSc Thesis, Departamento de Informática, FCUL , DI/FCUL, 2019. pdf
  • Nuno Burnay, Antónia Lopes, Vasco T. Vasconcelos. Safe(REST)Script, In Actas do 11º Encontro Nacional de Informática, INFORUM 2019. 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
  • Telmo Santos, Code Generation for RESTful APIs in HEADREST, MSc Thesis, Departamento de Informática, FCUL, DI/FCUL, July 2018. 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
  • Fábio Ferreira , Automatic Test Generation for RESTful APIs, MSc Thesis, Departamento de Informática, FCUL, DI/FCUL, 2017.  pdf
  • 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