Defines a condition that is belived to be true at certain point of function execution. Check condition being invalid, indicates that assumptions about program computation need to be revised. In effect, this indicates a bug in the implementation of the function. This bug is manifested by exceptionExContract.CheckException. Macro check can occure one or more times inside function definition.

Example:

@spec test_check(x :: integer) :: integer | no_return
def test_check(x) do
  r = x * x
  check r > x or r == 1
  r
end

The same as ExContract.check/1 but in addition accepts message paramter that gets embedded into ExContract.CheckException.

This macro is not meant to be called directly from client code; instead its invokation is made at compile time when it generates AST decorated with DbC constructs. This macro re-defines Kernel.def/2 and adds Design by Contract functionality to Elixir. When no pre or post-conditions are specified, this macro generates the same code as Kernel.def/2. When pre-conditions are specified, this macro insert the portion that adds the checks as the first statements that are executed. When post-coditions are specified the macro wraps the body of the function and stores the result into result variable that is avialable for examination in the definition of ExContract.ensures/1. The macro handles function definitions that contain implicit try block that is followed by rescue, after, or catch.

Example:

def without_even_trying do
  raise "oops"
after
  IO.puts "cleaning up!"
end

The same as ExContract.def/2 macro except add support for private functions.

Used for defining a benefit that a function guarantees to a client code. Establishes condition that is true when a function exits. Condition being false, upon a function exit, indicates a bug in the implementation of the function. This bug is manifested by exception ExContract.EnsuresException. Macro ensures can occure one or more times before function definition. By convention ensures macro is specified after requires is. This macro defines result variable that contains the returned result from the funciton used in specifying the post-condition.

Example:

ensures result == x * y
@spec test_ensures(x :: integer, y :: integer) :: integer | no_return
def test_ensures(x, y) do
  x * y
end

The same as ExContract.ensures/1 but in addition accepts message paramter that gets embedded into ExContract.EnsuresException.

Fail statement indicates that it is belived that a function excecution should never reach a portion of the code that contains the fail macro. Excecution of fail macro indicates that a particular path in function execution is possible and understanding of program control flow needs to be revised. In effect, this indicates a bug in the implementation of the function. This bug is manifested by exceptionExContract.FailException. Macro fail can occure one or more times inside function definition.

Example:

@spec test_fail(x :: integer) :: integer | no_return
def test_fail(x) do
  fail "This callback should never have been executed"
end

Defines a requirement that needs to be satisfied by a caller to a function in terms of pre-condition. A call to a function that specifies pre-condition is only valid if the condition parameter, upon method entry, is true. Parameter condition evaluating to false, is an indicatation of a bug in the caller. This bug is manifested by exception ExContract.RequiresException. Macro requires can occure one or more times before function definition. By convention requires macro is defined before ensures is.

Example:

requires x > 0
requires x < y, "Called with x=#{inspect x} and y=#{inspect y}"
@spec test_requires(x :: integer, y :: integer) :: integer | no_return
def test_requires(x, y) do
  ...
  ...
end

The same as ExContract.requires/1 but in addition accepts message paramter that gets embedded into ExContract.RequiresException.