jvoegele/bond

Design By Contract for Elixir

Bond

Design By Contract for Elixir.

Bond provides thorough support for contract programming (also known as "Design By Contract") for Elixir.

As described on Wikipedia:

Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing software.

It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants. These specifications are referred to as "contracts", in accordance with a conceptual metaphor with the conditions and obligations of business contracts.

The term was coined by Bertrand Meyer in connection with his design of the Eiffel programming language and first described in various articles starting in 1986 and the two successive editions (1988, 1997) of his book Object-Oriented Software Construction.

Design by contract has its roots in work on formal verification, formal specification and Hoare logic.

Bond applies the central ideas of contract programming to Elixir and provides support for attaching preconditions and postconditions to function definitions and conditionally evaluating them based on compile-time configuration.

Usage

Bond introduces two special annotations that can be used to define contracts for functions:

• @pre for defining function preconditions
• @post for defining function postconditions

Both of these annotations allow for attaching one or more assertions (with optional labels) to functions. These assertions are attached to functions at compile-time and evaluated at run-time.

To use these annotations and other features of Bond, you must use the Bond module in your own module(s). For example:

defmodule Math do
  use Bond

  @pre numeric_x: is_number(x), non_negative_x: x >= 0
  @post float_result: is_float(result),
        non_negative_result: result >= 0.0,
        "sqrt of 0 is 0": (x == 0) ~> (result === 0.0),
        "sqrt of 1 is 1": (x == 1) ~> (result === 1.0),
        "x > 1 implies result smaller than x": (x > 1) ~> (result < x)
  def sqrt(x), do: :math.sqrt(x)
end

The simple example above demonstrates how to define assertions in preconditions and postconditions. Assertions are simple boolean expressions, which have access to the bindings of the function that they precede. Assertions may have optional labels associated with them to aid in interpretation, either by human readers of the source code or in debugging assertion failures.

There are several variants of the syntax for assertions described in the section Assertion syntax below.

Assertions are evaluated at run-time; preconditions are evaluated prior to execution of the function body while postconditions are evaluated after the function, given that the function exits normally. Both preconditions and postconditions have access to the parameters of the function. Postconditions additionally have access to the result variable, which is bound to the result of the function, as well as old expressions (discussed in old expressions below).

Finally, Bond also provides a check/1 macro that can be used to place assertions at arbitrary points in the code. This facility can be used as a form of "sanity check" to verify that assumptions (about the state of the system or results of calculations, for example) hold true. Note, however, that these checks should not be used for verifying input data, data from external systems, or for any purpose for which if the check were removed it would compromise the integrity of the system. This is particularly true if these checks can be disabled via configuration.

use Bond {: .info}

When you use Bond, the Bond module will override several Kernel macros in order to support attaching preconditions and postconditions to functions. Specifically:

• Kernel.@/1 is overridden by Bond.@/1
• Kernel.def/2 is overridden by Bond.def/2
• Kernel.defp/2 is overridden by Bond.defp/2

use Bond will also import the Bond module so that the check/1 and check/2 macros are available for use.

Additionally, the Bond.Predicates module is automatically imported for all preconditions, postconditions, and checks, so that the predicate functions and operators that are defined therein can be used for assertions. Bond.Predicates can be explicitly imported into modules for use outside of assertions.

Assertion syntax

Assertions in Bond are conditional Elixir expressions, optionally associated with a textual label (either an atom or a string). These assertions may appear in @pre or @post expressions, or in calls to check/1 or check/2.

Bond offers considerable flexibility in its assertion syntax; assertions may take any of the following forms:

• expression - a "bare" expression without any associated label
• label, expression - an expression preceded by a string or atom label
• expression, label - an expression followed by a string or atom label
• label_1: expression_1, label_2: expression_2 - a keyword list with labels as the keys and expressions as the associated values

Bond also provides the Bond.Predicates module with predicates that are often useful in assertions. These include an "exclusive or" predicate and a logical implication predicate. The Bond.Predicates module is automatically imported for preconditions, postconditions, and check assertions. See the Bond.Predicates documentation for further details.

old expressions

old expressions allow postconditions to access the value of any arbitrary expression prior to execution of the function body. Postconditions are "pre-compiled" in such a way that any old expressions that appear in assertions are resolved to the value that they had at the start of function execution.

While this facility is not particularly relevant for purely functional code, it can be useful for stateful components of an application.

For example, imagine a simple, stateful Counter module that uses an Agent to store the current count (some Agent code omitted for brevity):

defmodule Counter do
  use Bond

  def get_count(agent) do
    Agent.get(agent, & &1)
  end

  @post count_incremented_by_1: get_count(agent) == old(get_count(agent)) + 1
  def increment_count(agent) do
    Agent.update(agent, &(&1 + 1))
  end
end

Notice how the old expression captures the value of get_count/1 prior to execution of the function, and this value is used to verify that the value of get_count/1 has been updated as expected.

Note, however, that there is a potential race condition in the above code. Since Agents are inherently concurrent, it is possible that another call to increment_count/1 is interleaved between execution of the function body and the call to get_count/1 that appears in the postcondition. In this scenario the postcondition would fail because the new value of get_count/1 would be at least 2 greater than the old value captured in the postcondition, rather than exactly 1 greater as specified in the count_incremented_by_1 assertion.

As a first attempt to alleviate this race condition we can update the increment_count/1 function so that it returns the updated count as its result and use that result in the postcondition directly:

  @post returns_updated_count: result == old(get_count(agent)) + 1
  def increment_count(agent) do
    Agent.get_and_update(agent, fn count ->
      new_count = count + 1
      {new_count, new_count}
    end)
  end

In this version we utilize Agent.get_and_update/3 to update the counter and return the updated counter value in one operation. The new counter value is the result of the function which can be used in postconditions. The returns_updated_count assertion compares this result to the old value of get_count/1 to ensure that it was incremented by exactly 1.

However, as you may have noticed, it is still possible for another call to increment_count/1 to be interleaved between the call to get_count/1 in the old expression of the postcondition and the call to Agent.get_and_update/3 in the function body. Alas, there is no way to "lock" an Agent over multiple operations to ensure that there are no concurrent updates to the Agent state. Therefore, our only choice is to soften the guarantee made by our postcondition:

  @post count_increased: get_count(agent) > old(get_count(agent))
  def increment_count(agent) do
    Agent.update(agent, &(&1 + 1))
  end

The count_increased assertion in the postcondition now guarantees only that the new value of get_count/1 is strictly greater than the old value. This assertion always holds true regardless of the number of concurrent state updates to the counter.

Although this assertion is not as strong as the count_incremented_by_1 assertion in the original version, it is the strongest we can provide given the possibility of concurrent state updates.

Future versions of Bond may provide stronger support for stateful contracts in the form of invariants for structs and/or stateful processes, although this is still a subject of research.

Documenting contracts

Contracts in the form of preconditions and postconditions are part of the public interface for a module in the same way that function signatures and typespecs are. Therefore, it is essential that contracts are included as part of the documentation for modules and functions.

Bond automatically appends Preconditions and Postconditions section to the documentation for any function that defines any preconditions or postconditions and has a @doc attribute. These two generated sections include all of the assertions specified in the function contract as nicely formatted Elixir code. Furthermore, contract documentation is generated even if run-time assertion checking is disabled via configuration. Therefore, it is not necessary to explicitly document preconditions or postconditions in the @doc for a function unless greater detail is warranted.

The contract documentation is visible not only in documentation generated by ex_doc but also in code editing environments that are able to display function docs directly in the editor, such as with the K command in Vim or on mouse hover in VS Code.

Installation

bond can be installed by adding it to your list of dependencies in mix.exs:

def deps do
  [
    {:bond, "~> 0.8.3"}
  ]
end

Documentation

Documentation is generated with ExDoc and published on HexDocs and be found at https://hexdocs.pm/bond/Bond.html.