# Corsa
`Corsa` is a library to write executable code contracts in Elixir.
## Installation
The package can be installed by adding `corsa` to your list of dependencies in `mix.exs`:
```elixir
def deps do
[
{:corsa, git: "git@gitlab.com:babel-upm/corsa.git", branch: "main"}
]
end
```
## Contracts
Corsa contracts are written using normal pre- and post-condition contracts familiar from other
programming languages and libraries such as Eiffel. To use the library in a module we must first
insert a
```elixir
use Corsa
```
statement in the module. Suppose next that we have implemented a function `list_to_nat` which
converts an integer represented as a list of small numbers (between 0 and 9) to an integer:
Suppose next that we have implemented a function `list_to_nat` which converts an integer
represented as a list of small numbers (between 0 and 9) to an integer. We can require that the
argument to `list_to_nat` is correct by specifying a `@pre` contract:
```elixir
iex> defmodule Example do
...> use Corsa
...> @pre list_to_nat(l), do: is_decimal_list(l)
...> @post list_to_nat(l), do: is_integer(result)
...> def list_to_nat(list), do: list_to_nat(list, 0)
...> defp list_to_nat([], result), do: result
...> defp list_to_nat([ n| rest ], acc) do
...> list_to_nat(rest ,10*acc+n)
...> end
...> defp is_decimal_list([n|rest]) do
...> is_decimal(n) and (n > 0)
...> and Enum.all?(rest,&is_decimal/1)
...> end
...> defp is_decimal_list(_), do: false
...> defp is_decimal(n) do
...> is_integer(n) and (n >= 0) and (n < 10)
...> end
...> end
iex> Example.list_to_nat([1,5])
15
iex> Example.list_to_nat(5)
** (Corsa.PreViolationError) @pre does not hold in call 'CorsaDoctestTest.Example.list_to_nat(5)'
```
If we now invoke the function with an incorrect argument by default an informative exception is
raised.
Similarly `@post` contracts check that the value returned by a function is correct:
## Assertions
Assertions can be stated using the `@assert` construct:
```elixir
iex> defmodule Example do
...> use Corsa
...> def f(y) do
...> x = g(y)
...> @assert x > 0
...> x + 10
...> end
...> defp g(x) do x end
...> end
iex> Example.f(10)
20
iex> Example.f(-10)
** (Corsa.AssertViolationError) @assert does not hold in expression 'x > 0' with values: 'x = -10'
```
## Termination Guarantees
Corsa can check whether recursive functions eventually terminate, through specifying a measure
using the `@decreases` construct:
```elixir
iex> defmodule Example do
...> use Corsa
...> @decreases sum(l), do: length(l)
...> def sum([]), do: 0
...> def sum([n|rest]), do: n+sum(rest)
...> end
iex> Example.sum([1,2,3])
6
```
The `@decreases` annotation specifies a function, that when applied to the arguments of the called
function, calculates a measure (e.g., an integer). Corsa checks that measure when a function is
invoked is strictly greater than the measure in recursive calls. In the example above, the
measure used is the length of the least which strictly decreases in recursive calls. The check
will be made even if the recursive call is made within another function.
Note, however, that a decreasing measure does not necessarily guarantee termination:
```elixir
defmodule Example do
use Corsa
@decreases fact(n), do: n
def fact(1), do: 1
def fact(n), do: n * fact(n - 1)
end
```
If the function is invoked with `fact(-1)` then it obviously never terminates (except possibly
with an exception) but the measure always strictly decreases. Note you can "fix" the previous
contract by using `abs/1`:
```elixir
iex> defmodule Example do
...> use Corsa
...> @decreases fact(n), do: abs(n)
...> def fact(1), do: 1
...> def fact(n), do: n * fact(n - 1)
...> end
iex> Example.fact(10)
3628800
iex> Example.fact(0)
** (Corsa.DecreasesViolationError) @decreases does not hold, call 'CorsaDoctestTest.Example.fact(-1)' does not decrease after 'CorsaDoctestTest.Example.fact(0)'
```
## Time Contracts
Time bounds for long a function application may execute can be specified with the `@within`
construct:
```elixir
defmodule Example do
use Corsa
@within fact(n), do: 2000
def fact(1), do: 1
def fact(n), do: n*fact(n-1)
end
```
If the call to the factorial function does not return an answer within 2000 milliseconds, an error
is logged.
## Message Passing Contracts
The `@expects` contract specifies the accepatble messages in a receive statement.
```elixir
iex> defmodule Example do
...> use Corsa
...>
...> def counter(state) do
...> @expects [v > 0, receive do
...> :inc -> counter(state + 1)
...> :dec -> counter(state - 1)
...> {:set, v} -> counter(v)
...> end]
...> end
...> end
iex> send(self(), :inc)
iex> send(self(), {:set, 10})
iex> send(self(), {:set, -1})
iex> Example.counter(0)
** (Corsa.ExpectsViolationError) @expects does not hold in expression 'v > 0' with values: 'v = -1'
```
## Type Contracts
When using `Corsa` type annotations will be used to generate runtime typechecks for your
functions.
```elixir
iex> defmodule Example do
...> use Corsa
...>
...> @spec id(integer()) :: integer()
...> @spec id(boolean()) :: boolean()
...> def id(x) do x end
...> end
iex> Example.id(10)
10
iex> Example.id(true)
true
iex> Example.id("hello")
** (Corsa.SpecArgViolationError) @spec does not hold in arguments in call 'CorsaDoctestTest.Example.id("hello")'
```
## Configuring Corsa
Corsa can be configured to either (the default) raise exceptions whenever a contract is violated,
or log contract violations, or do nothing.
To disable Corsa:
```elixir
defmodule Example do
use Corsa, disabled: true
...
end
```
To log contracts, you must specify the logging level:
```elixir
defmodule Example do
use Corsa, logger: :error
...
end
```
When logging is enabled, contracts can be executed asynchronously. To enable asynchronous execution:
```elixir
defmodule Example do
use Corsa, logger: :error, async: true
end
```
Global configuration can be performed through the configuration file located at `config/config.exs`:
```elixir
config :corsa, disabled: true
```
