View Source Corsa.StateM.Post (corsa v0.1.2)
Postconditions are essential conditions that must be fulfilled following the execution of a function, thereby assuring that the anticipated output conditions have been met. In Corsa, postconditions are evaluated during runtime. If a postcondition isn't guaranteed, an exception or log is generated. Within the definition of a state machine, postconditions are able to access the state.
Summary
Functions
Errors
iex> defmodule Elixir.Corsa.StateM.Post.ExampleError1 do
...> use Corsa.Assert
...> use Corsa.StateM.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.StateM.Post.ExampleError2 do
...> use Corsa.Assert
...> use Corsa.StateM.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.StateM.Post.ExampleError3 do
...> use Corsa.Assert
...> use Corsa.StateM.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.StateM.Post.ExampleError4 do
...> use Corsa.Assert
...> use Corsa.StateM.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
iex> defmodule Elixir.Corsa.StateM.Post.ExampleError4 do
...> use Corsa.Assert
...> use Corsa.StateM.Post
...> post f(x, state) 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.StateM.Post.ExampleError1 do
...> use Corsa.Assert
...> use Corsa.StateM.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.StateM.Post.ExampleError2 do
...> use Corsa.Assert
...> use Corsa.StateM.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.StateM.Post.ExampleError3 do
...> use Corsa.Assert
...> use Corsa.StateM.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.StateM.Post.ExampleError4 do
...> use Corsa.Assert
...> use Corsa.StateM.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
iex> defmodule Elixir.Corsa.StateM.Post.ExampleError4 do
...> use Corsa.Assert
...> use Corsa.StateM.Post
...> post f(x, state) do x > y end
...> def f(x, y) do x + y end
...> end
** (Corsa.PostError) result cannot be an argument in @post