View Source 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:

def deps do
  [
    {:corsa, "~> 0.1.2"}
  ]
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:

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:

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:

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:

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:

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:

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:

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.

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.

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:

defmodule Example do
  use Corsa, disabled: true
  ...
end

To log contracts, you must specify the logging level:

defmodule Example do
  use Corsa, logger: :error
  ...
end

When logging is enabled, contracts can be executed asynchronously. To enable asynchronous execution:

defmodule Example do
  use Corsa, logger: :error, async: true
end

Global configuration can be performed through the configuration file located at config/config.exs:

config :corsa, disabled: true