View Source Corsa (corsa v0.1.2)

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 AssertExample do
...>   use Corsa
...>   def f(y) do
...>     x = g(y)
...>     @assert x > 0
...>     x + 10
...>   end
...>   defp g(x) do x end
...> end
iex> AssertExample.f(10)
20
iex> AssertExample.f(-10)
** (Corsa.AssertViolationError) @assert does not hold in expression 'x > 0' with values left '-10' and right '0'

Termination Guarantees

Corsa can check whether recursive functions eventually terminate, through specifying a measure using the @decreases construct:

iex> defmodule DecreasesExample1 do
...>   use Corsa
...>   @decreases sum(l), do: length(l)
...>   def sum([]), do: 0
...>   def sum([n|rest]), do: n+sum(rest)
...> end
iex> DecreasesExample1.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 DecreasesExample2 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 DecreasesExample3 do
...>   use Corsa
...>   @decreases fact(n), do: abs(n)
...>   def fact(1), do: 1
...>   def fact(n), do: n * fact(n - 1)
...> end
iex> DecreasesExample3.fact(10)
3628800
iex> DecreasesExample3.fact(0)
** (Corsa.DecreasesViolationError) @decreases does not hold, call 'CorsaDoctestTest.DecreasesExample3.fact(-1)' does not decrease, previous measure: '0', new measure: '1'

Time Contracts

Time bounds for long a function application may execute can be specified with the @within construct:

iex> defmodule WithinExample do
...>   use Corsa
...>   @within f(n) do n end
...>   def f(n) do Process.sleep(n + 10) end
...> end
iex> WithinExample.f(1)
** (Corsa.WithinViolationError) @within does not hold in call 'CorsaDoctestTest.WithinExample.f(1)'

If the call to f function does not return an answer within n + 10 milliseconds, an error is logged.

Message Passing Contracts

The @expects contract specifies the accepatble messages in a receive statement.

iex> defmodule ExpectsExample 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> ExpectsExample.counter(0)
** (Corsa.ExpectsViolationError) @expects does not hold in expression 'v > 0' with values left '-1' and right '0'

Variable Contracts

Variable contracts allow you to define variable contracts. In Corsa, these contracts restrict the values that may be assigned to a variable.

# iex> defmodule DeclareExample do
# ...>   use Corsa
# ...>   @declare is_integer(n) && n > 0
# ...>   def counter(n) do
# ...>     receive do
# ...>       :inc -> counter(n + 1)
# ...>       :dec -> counter(n - 1)
# ...>       {:set, n} -> counter(n)
# ...>     end
# ...>   end
# ...> end
# iex> send(self(), :inc)
# iex> send(self(), {:set, 10})
# iex> send(self(), {:set, -1})
# iex> DeclareExample.counter(0)

Type Contracts

When using Corsa type annotations will be used to generate runtime typechecks for your functions.

iex> defmodule TypedExample do
...>   use Corsa
...>   @spec id(integer()) :: integer()
...>   @spec id(boolean()) :: boolean()
...>   def id(x) do x end
...> end
iex> TypedExample.id(10)
10
iex> TypedExample.id(true)
true
iex> TypedExample.id("hello")
** (Corsa.SpecArgViolationError) @spec does not hold in arguments in call 'CorsaDoctestTest.TypedExample.id("hello")'

State Contracts

iex> defmodule StateExample do
...>   use Corsa, state: true
...>   @init :not_started
...>
...>   @next start(), do: 0
...>   @throws start(), do: not started?(:not_started)
...>   def start() do
...>     try do
...>       :ets.new(:counter, [:named_table])
...>       :ets.insert(:counter, {"value", 0})
...>       :ok
...>     catch
...>       _, _ -> raise "error already started"
...>     end
...>   end
...>
...>   @next inc(), do: state + 1
...>   @throws inc(), do: started?(state)
...>   def inc() do
...>     [{"value", v}] = :ets.lookup(:counter, "value")
...>     :ets.insert(:counter, {"value", v + 1})
...>     :ok
...>   end
...>
...>   @throws get(), do: started?(state)
...>   def get() do
...>     [{"value", v}] = :ets.lookup(:counter, "value")
...>     v
...>   end
...>   def started?(state), do: state != :not_started
...> end
iex> StateExample.start()
iex> StateExample.inc()
iex> StateExample.inc()
iex> StateExample.get()
2
iex> StateExample.start()
** (RuntimeError) error already started

Monitors

Configuring Corsa

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

Logging levels

iex> defmodule LogsExample do
...>   use Corsa, logger: :error
...>   @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

Disabling contracts

iex> defmodule DisabledContracts do
...>   use Corsa, disabled: true
...>   @pre f(x), do: x > 0
...>   @post f(x), do: result > 0
...>   def f(x), do: x
...> end
iex> DisabledContracts.f(-1)
-1