# Corsa

`Corsa` is a library to write runnable 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
````
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:
````
iex(1)> list_to_nat([5])
5

iex(2)> list_to_nat([5,1,7])
517
````
We can require that the argument to `list_to_nat`
is correct by specifying a `@pre` contract:
````
@pre list_to_nat(l), do: is_decimal_list(l)
def list_to_nat(l) do
  ...
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
````
If we now invoke the function with an incorrect argument by
default an informative exception is raised:
````
iex(3)> Cex2.list_to_nat(5)
** (Corsa.PreViolationError) @pre does not hold in call 'Cex2.list_to_nat(5)'
````

Similarly `@post` contracts check that the value returned by
a function is correct:
````
@post list_to_nat(l), do: is_integer(result)
def list_to_nat(l) do
  ...
end  
````

## Assertions

Assertions can be stated using the `@assert` construct:
````
def f(y) do
  x = g(y)
  @assert x>0
  h(x)
end
````

## Termination Guarantees

Corsa can check whether recursive functions eventually terminate, through
specifying a measure using the `@decreases` construct:
````
@decreases(l), do: length(l)
def sum([]), do: 0
def sum([n|rest]), do: n+sum(rest)
````
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:
````
@decreases(l), do: n
def fact(1), do: 1
def fact(n), do: n*fact(n-1)
````
If the function is invoked
with
````
iex> fact(-1)
````
then it obviously never terminates (except possibly with an exception)
but the measure always strictly decreases.

## Time Contracts

Time bounds for long a function application may execute can
be specified with the `@within` construct:
````
@within fact(n), do: 2000
def fact(1), do: 1
def fact(n), do: n*fact(n-1)
````
If the call to the factorial function does not return an answer
within 2000 milliseconds, an error is logged. 

## Integration with TypeCheck

Corsa can use the TypeCheck runtime type checking library
type checking facilities.
If we for example want to check that a function only receives
arguments that are prime numbers we can do that through
specifying a TypeCheck type guard using the `@type!` construct:
````
@type! key :: integer when is_prime(key)

@spec encrypt(key(), binary()) :: binary()
def encrypt(k, msg) do
 ...
end

@spec encrypt(key(), binary()) :: binary()
def decrypt(k, msg) do
 ...
end
````
That is, first we define a new type `key` specifying that it is
an integer, and, as an additional constraint, that it must
satisfy the `is_prime` type guard (an arbitrary function).
Then we can specify that functions such as `encrypt` and `decrypt`
receive proper keys as arguments, and if they do not, an exception
will be raised at runtime.
Note however that in the current version of TypeCheck this works
only if both the type declaration and its use is made in the same
module, or if the guard function inside the `@type` construct
is specified with a fully qualified module name (and the function
is an exported one).

## Configuring Corsa

Corsa can be configured to either (the default) raise exceptions
whenever a contract is violated, or log contract violations,
or do nothing.