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:

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.