View Source Corsa.Post (corsa v0.1.2)
Postconditions are specifications which must be fulfilled after the execution of a function, thereby certifying that the anticipated output criteria have been satisfied. In Corsa, postconditions are evaluated at runtime. If a postcondition is not satisfied, either an exception or a log is generated.
Example
iex> defmodule Elixir.Corsa.Post.Example do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, y) do result > x end
...> def f(x, y) do x + y end
...> end
iex> Elixir.Corsa.Post.Example.f(2, 1)
3
iex> Elixir.Corsa.Post.Example.f(1, -1)
** (Corsa.PostViolationError) @post does not hold in call 'Corsa.Post.Example.f(1, -1)' with result '0'Summary
Functions
Errors
iex> defmodule Elixir.Corsa.Post.ExampleError1 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, y) do x > y end
...> post f(x, y) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) @post for function 'f/2' already defined
iex> defmodule Elixir.Corsa.Post.ExampleError2 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, x) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) arguments in @post should contain different names
iex> defmodule Elixir.Corsa.Post.ExampleError3 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, _) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) arguments in @post cannot be ignored with _
iex> defmodule Elixir.Corsa.Post.ExampleError4 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, result) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) result cannot be an argument in @postFunctions
Errors
iex> defmodule Elixir.Corsa.Post.ExampleError1 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, y) do x > y end
...> post f(x, y) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) @post for function 'f/2' already defined
iex> defmodule Elixir.Corsa.Post.ExampleError2 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, x) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) arguments in @post should contain different names
iex> defmodule Elixir.Corsa.Post.ExampleError3 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, _) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) arguments in @post cannot be ignored with _
iex> defmodule Elixir.Corsa.Post.ExampleError4 do
...> use Corsa.Assert
...> use Corsa.Post
...> post f(x, result) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) result cannot be an argument in @post