A REST API defines how clients can access and manipulate representations of resources, identified by Unique Resource Identifiers, by using the operations offered by HTTP.
POST /person/{name}
GET /person/{name}
GET /person/{name}/friends/{friend}
PUT /person/{name}
DELETE /person/{name}/friends/{friend}
In this tutorial, we will use an example of a very simple REST API with five endpoints that allow to access and manipulate a single type of resource - Person. Persons are identified by URIs that adhere to the template "/person/{name}". A textual representation of a person at a given point in time, obtained with a call to the first endpoint, is shown below.
{
name: "Manel",
age: 23,
friends: ["Paulo", "João"]
}
An API without documentation is not useful. In this tutorial we show how we can use HeadREST to formally describe the behaviour of our example API. The behaviour of the service at each endpoint is specified by one or more assertions of the form {pre-condition} method uri-template {post-condition}. An assertion states that if a call to that endpoint is executed in a state that satisfies the pre-condition, then it should terminate in a state that satisfies the post-condition. In our example, as shown below, we will define one assertion for each endpoint.
{...} post `/person/{name}` {...}
{...} get `/person/{name}` {...}
{...} post `/person/{name}/friends/{friend}` {...}
{...} put `/person/{name}` {...}
{...} delete `/person/{name}/friends/{friend}` {...}
A HeadRest specification declares the resources that can be accessed and manipulated through the API. The specification can also include definition of data types that are useful to characterise the data sent in requests or received in the responses in the different endpoints. Particularly useful is the definition of types that are declared to represent a particular resource type.
specification Types
resource Person
type PersonData represents Person = {
name: (x: String where size(x) >= 3),
age: (x: Integer where x >= 0),
friends: String[]
}
type InputData = {
name: (x: String where size(x) >= 3),
friend: (x: String where size(x) >= 3)
}
type OptionalData = {
?metadata: String
}
Resource types enable us to reason about collections of entities in the specification. Resource type declarations can declare one or more resources. For instance, the declaration resource A, B, C simultaneously declares three resource types. Note that the represents keyword is not obligatory in type declarations that represent resources.
In our example we see that the type PersonData is declared to be the type of the representations of the resource Person. Notice the use of refinement types to express that age is a natural number and that the name must have at least three characters. The PersonData type is an object type, declared as type ObjectType = {...}, however types can also be aliases for other types. For example, the type Natural can be defined as, type Natural = (x : Integer where x >= 0).
In the OptionalData type, we see a field with a preceding question mark, this signifies that this field is optional. To use optional fields we must first state that they are defined. There are two ways of achieving this, through the isdefined predicate and through the in operator, as illustrated below.
isdefined(optionalData.metadata)
optionalData in {metadata: String}
Both properties hold only if the optionalData has the field metadata.
Conditions in assertions, besides the state of the system, address the data sent by the client in the request and the data sent back by the service in the response. In HeadREST, variables request and response serve to refer to this data, i.e., to the input and output of a call to an operation exposed in an endpoint. The types for these variables are shown below.
The type of the request reflects that the parameters used in the URI template of an endpoint are encapsulated in the field template; additional data can be sent in the request body and headers. The type of the response reflects that the response carries a response status code indicating whether the request has been successfully completed and might additionally carry other data in the body and headers.
type Request = {
location: String,
?template: {},
header: {},
?body: Any
}
type Response = {
code: Integer,
header: {},
?body: Any
}
The use of the variables request and response in the context of an assertion is illustrated below. This assertion expresses that if the data sent in the request template is of type InputData, then the response is guaranteed to contain the success code and the data in the response body belongs to the requested friend.
{
request.template in InputData
}
get `/person/{name}/friends/{friend}`
{
response.code == 200 &&
response in {body: PersonData} &&
response.body.name == request.template.friend
}
HeadREST has the iterators foreach and forsome to express universal/existential properties concerning the elements of an array. We illustrate the use of forsome in the condition presented below.
(forsome friend of response.body.friends ::
friend.name == request.template.name
)
We could include this property in the post-condition of the previous example. This would mean that the request.template.name is included in the friends list of the current friend.
HeadREST has two binary operators to reason about resources - repof and uriof. The expression t repof r states that a data value t is a representation of resource r and u uriof r states that a string u is a URI of resource r.
As illustrated below, these two operators allow us to specify important properties, such as: the value in data is a representation of the resource in person, and the String on the left side of the uriof expression is a URI of the resource in person.
data repof person &&
("/person/" ++ request.template.name) uriof person && ...
To reason about collections of data values and resources, HeadREST provides universal (forall) and existential (exists) quantifiers. Quantifiers are quite common and useful to express properties concerning the state of the system before and after the execution of an operation exposed by an endpoint.
For instance, in the assertion below, they allow us to express that, if there isn't already a person with the name provided in the request and the age being provided is greater or equal to 18, then the request is successful and it is ensured that there is a person with the name and age that was provided in the request.
{
request.template in {name: String} &&
request in {body: {age: Integer}} &&
(forall person : Person ::
(exists data : PersonData ::
data repof person &&
data.name != request.template.name
)
) &&
request.body.age >= 18
}
post `/person/{name}`
{
response.code == 201 &&
(exists person : Person ::
(exists data : PersonData ::
data repof person &&
data.name == request.template.name &&
data.age == request.body.age &&
data.friends == []
)
)
}
It is possible to express iterators using quantifiers. The example presented in the iterators section could alternatively be written as follows:
(exists i : (x : Natural where x < length(response.body.friends)) ::
response.body.friends[i].name == request.template.name
)
HeadREST has some built-in functions, such as length (for arrays), size (for strings), matches (for strings and regular expressions), isdefined (for checking the existence of optional fields) and expand (for expanding a URI template to a URI, once values for the template parameters are provided).
{
request.template in {name: String} &&
(exists person : Person ::
expand(`/person/{name}`,
{name = request.template.name}
) uriof person
)
}
get `/person/{name}`
{
response.code == 200 &&
response in {body: PersonData} &&
response.body.name == request.template.name
}
As illustrated in this example, the second argument of the expand function is an object with the values of the parameters (marked by "{}") present in the URI given in the first argument. This allows us to reason about the URIs of resources. Another function already used in a previous example is the length function which receives an array and allows us to reason about its size.
This assertion states that, if there is a person in the target URI, then the response code is 200 and includes its representation in the body.
Often, resources have a single representation of a given type. In this case, the extract operator, represented by a single quotation mark ('), simplifies the access to such representation: we use r' to denote the representation of the resource r.
Take note that to use the extract operator on a resource there must be exactly one type which represents that resource. In our example, only type PersonData declares that represents Person, therefore we can use the extract operator on resources with type Person.
The example below illustrates the use of this operator as well as the foreach/forsome in our running example which declares that resources of type Person have a single representation of type PersonData.
{
request.template in InputData &&
(exists person : Person ::
person'.name == request.template.name &&
(forsome friendName of person'.friends ::
friendName == request.template.friend
)
)
}
delete `/person/{name}/friends/{friend}`
{
response.code == 200 &&
(exists person : Person ::
person'.name == request.template.name &&
(foreach friendName of person'.friends ::
friendName != request.template.friend
)
)
}
This assertion specifies that if there is a person with request.template.name that has a friend with name request.template.friend, then the request is successful and it is ensured that there is a person with the name request.template.name that does not have a friend with the name request.template.friend.
It is also possible to simplify the post-condition of the assertion presented in the quantifiers section by using the extract operator on resource person:
(exists person : Person ::
person'.name == request.template.name &&
person'.age == request.body.age &&
person'.friends == []
)
Interpolation allows to express an expansion of a URI template (substitute templates for expressions). Interpolation is expressed with a special string with single quotes that starts with $ and can contain expressions inside curly brackets to indicate how parameters are instantiated.
{
request.template in {name: String} &&
request in {body: {friend: String}} &&
(exists person : Person ::
$'/person/{request.template.name}' uriof person &&
(foreach name of person'.friends ::
request.body.friend != name
)
) &&
(exists friend : Person ::
$'/person/{request.body.friend}' uriof friend
)
}
put `/person/{name}`
{
response.code == 201 &&
(exists person : Person ::
person'.name == request.template.name &&
(forsome name of person'.friends ::
request.body.friend == name
)
)
}
In the assertion above interpolation is used in pre-condition to require the existence of a person in the target URL. In the pre-condition we ascertain the existence of a person with the name request.template.name that does not have a friend with the name request.body.friend. We also state the existence of a person with the name request.body.friend. If the pre-condition holds, it is guaranteed that the target person, with name request.template.name, gets a new friend with name request.body.friend.
Interpolation can be emulated with the expand function. The underlined interpolation present in the assertion above is equivalent to the expand function in the pre-condition of the assertion presented in the built-in functions section.
We can declare global variables that can be used in several assertions.
In the quantifiers section we saw an example that specifies the creation of new persons. Another way to express that example, making use of global variables, is the following:
var person: Person
{
request.template in {name: String, age: Integer} &&
(exists data: PersonData ::
data repof person &&
data.name != request.template.name
) &&
request.template.age >= 18
}
post `/person/{name}`
{
response.code == 201 &&
(exists data: PersonData ::
data repof person &&
data.name == request.template.name &&
data.age == request.template.age &&
data.friends == []
)
}
In this assertion the variable person refers to the same resource in both the pre-condition and the post-condition. Global variables allow us to retain knowledge across different scopes.
In HeadREST it is also possible to create user-defined functions and predicates. This enables the abstraction of patterns and reduces repetition across the specification. The assertion for the endpoint get `/person/{name}` shown below illustrates the use of a predicate defined as follows.
predicate existsInputData(input: InputData) =
exists person: Person ::
expand(`/person/{name}`, {name = input.name}) uriof person &&
(exists friend: Person ::
$'/person/{input.friend}' uriof friend
)
A predicate is a special case of a function. A predicate always returns a Boolean. If this predicate was a function the signature would be the following: function existsInputData(input: InputData) : Boolean.
An example of the predicate above being used can be seen below:
{
request.template in InputData &&
existsInputData(request.template)
}
get `/person/{name}/friends/{friend}`
{
response.code == 200 &&
response in {body: PersonData} &&
response.body.name == request.template.friend
}
In the area of security, principal is a term used to designate an entity that uses the system and can be authenticated. To be able to refer to these entities, HeadREST provides the Principal type. To use the Principal type, HeadREST has the principalof uninterpreted function. This uninterpreted function has one argument of type Any and returns either a Principal, denoting a successful authentication, or null otherwise.
Below we present an example of an assertion that specifies the behaviour of the endpoint get `/person/{name}` when, in the header of the request is sent an Api Key that authenticates a principal.
var princip: Principal
{
request.template in {name: String} &&
request.header in {api_key: String} &&
princip == principalof(request.header.api_key) &&
...
}
get `/person/{name}`
{
response.code == 200 &&
...
}
In order to model authorisation policies, HeadREST also supports the introduction of user-defined uninterpreted functions. These functions give us the ability to relate the elements of the Principal type with values of other types.
Below we present an example of an assertion for an API with security policies that depend on OAuth 2.0 and scopes. The assertion states that, when in the header of the request, is sent an authentication element that authenticates a principal that has the scope "write", then the request is successful.
type Scope = ["read"]|["write"]
var princip: Principal
predicate hasScope(p: Principal, s: Scope)
{
request.template in {name: String} &&
request.header in {Authorization: String} &&
princip == principalof(request.header.Authorization) &&
hasScope(princip, "write") &&
...
}
post `/person/{name}`
{
response.code == 201 &&
...
}
Below we present a specification for the example, which puts together some of the elements presented before.
specification PersonAPI
resource Person
type PersonData represents Person = {
name: (x : String where size(x) >= 3),
age: (x : Integer where x >= 0),
friends: String[]
}
type InputData = {
name: (x : String where size(x) >= 3),
friend: (x : String where size(x) >= 3)
}
type OptionalData = {
?metadata: String
}
{
request.template in {name: String} &&
request in {body: {age: Integer}} &&
(forall person : Person ::
(exists data : PersonData ::
data repof person &&
data.name != request.template.name
)
) &&
request.body.age >= 18
}
post `/person/{name}`
{
response.code == 201 &&
(exists person : Person ::
person'.name == request.template.name &&
person'.age == request.body.age &&
person'.friends == []
)
}
{
request.template in {name: String} &&
(exists person : Person ::
expand(`/person/{name}`,
{name = request.template.name}
) uriof person
)
}
get `/person/{name}`
{
response.code == 200 &&
response in {body: PersonData} &&
response.body.name == request.template.name
}
{
request.template in InputData &&
(exists person : Person ::
expand(`/person/{name}`,
{name = request.template.name}
) uriof person &&
(exists friend : Person ::
$'/person/{request.template.friend}' uriof friend
)
)
}
get `/person/{name}/friends/{friend}`
{
response.code == 200 &&
response in {body: PersonData} &&
response.body.name == request.template.friend
}
var person: Person
{
request.template in InputData &&
person'.name == request.template.name &&
(forsome friendName of person'.friends ::
friendName == request.template.name
)
}
delete `/person/{name}/friends/{friend}`
{
response.code == 200 &&
person'.name == request.template.name &&
(foreach friendName of person'.friends ::
friendName != request.template.friend
)
}
{
request.template in {name: String} &&
request in {body: {friend: String}} &&
(exists person : Person ::
$'/person/{request.template.name}' uriof person &&
(foreach name of person'.friends ::
request.body.friend != name
)
) &&
(exists friend : Person ::
$'/person/{request.body.friend}' uriof friend
)
}
put `/person/{name}`
{
response.code == 201 &&
(exists person : Person ::
person'.name == request.template.name &&
(forsome name of person'.friends ::
request.body == name
)
)
}