View Source Corsa.Decreases (corsa v0.1.2)
The decreases contract 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.
Example
iex> defmodule Elixir.Corsa.Decreases.Example do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(n) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
iex> Elixir.Corsa.Decreases.Example.fact(10)
** (Corsa.DecreasesViolationError) @decreases does not hold, call 'Corsa.Decreases.Example.fact(1)' does not decrease, previous measure: '0', new measure: '1'Summary
Functions
Errors
iex> defmodule Elixir.Corsa.Decreases.ExampleError1 do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(n) do n end
...> decreases fact(n) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
** (Corsa.DecreasesError) @decreases for function 'fact/1' already defined
iex> defmodule Elixir.Corsa.Decreases.ExampleError2 do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(n, n) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
** (Corsa.DecreasesError) arguments in @decreases should contain different names
iex> defmodule Elixir.Corsa.Decreases.ExampleError3 do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(_) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
** (Corsa.DecreasesError) arguments in @decreases cannot be ignored with _Functions
Errors
iex> defmodule Elixir.Corsa.Decreases.ExampleError1 do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(n) do n end
...> decreases fact(n) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
** (Corsa.DecreasesError) @decreases for function 'fact/1' already defined
iex> defmodule Elixir.Corsa.Decreases.ExampleError2 do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(n, n) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
** (Corsa.DecreasesError) arguments in @decreases should contain different names
iex> defmodule Elixir.Corsa.Decreases.ExampleError3 do
...> use Corsa.Assert
...> use Corsa.Decreases
...> decreases fact(_) do n end
...> def fact(0) do fact(1) end
...> def fact(n) do n * fact(n - 1) end
...> end
** (Corsa.DecreasesError) arguments in @decreases cannot be ignored with _