Bond - Design by Contract for Elixir

Announcing Bond, Design by Contract for Elixir

Bond provides support for contract programming (also known as “Design by Contract”) for Elixir.

The primary goal for Bond is to provide the most feature-complete and thoroughly documented Design by Contract library for Elixir, with a concise and flexible syntax for specifying contracts.

Current and planned features include:

  • Function preconditions with @pre
  • Function postconditions with @post
  • “old” expressions in postconditions
  • “check” expressions for arbitrary assertions within a function body
  • Predicates (such as implies? and xor) for use in assertions
  • Detailed assertion failure reporting
  • Incorporation of preconditions and postconditions into @doc for function
  • Conditional compilation of contracts per environment
  • More detailed assertion failure reporting, including color coding à la ExUnit
  • Invariants for structs and/or stateful processes (if possible)

For comparison to other Design by Contract libraries for Elixir, please see the history section of the Bond documentation.

https://hexdocs.pm/bond/

11 Likes

Hi–

Interesting project. I saw this in the docs:

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.

Is the intention that pre/post conditions replace traditional typespecs when used or should they be considered supplemental? If they are a replacement, do they interact with Dialyzer at all? Also, the set-theoretic types, assuming they land, also offer a manner of contract with functionality ramifications, are there thoughts about how this library would relate to that future?

I’ve not looked much beyond a quick search through the docs. But these are the questions I’d need to understand for adoption.

2 Likes

Hi @sbuttgereit,

Contracts are not intended to replace typespecs or set-theoretic types; rather, they are complementary mechanisms.

Typespecs are evaluated at compile-time or with a static analysis tool such as Dialyzer, whereas contracts as implemented by Bond are evaluated at run-time (although they are attached to functions at compile-time so must be valid Elixir code).

The closest analogue to contracts in native Elixir is guard expressions for functions, which allow for making rudimentary “assertions” about function arguments. Assertions in Bond are much more powerful and are not limited to the pre-defined set of functions that are allowed in guard expressions.

2 Likes

@sbuttgereit:

The closest analogue to contracts in native Elixir is guard expressions for functions, which allow for making rudimentary “assertions” about function arguments. Assertions in Bond are much more powerful and are not limited to the pre-defined set of functions that are allowed in guard expressions.

Also note that even if a particular assertion could be implemented as a guard clause or pattern match on a function head, if you are using Bond it might be preferable to implement those assertions as preconditions to the function instead. The reason being is that Bond will provide a much clearer error message if a particular assertion fails, as opposed to a FunctionClauseError which would be more difficult to interpret.

Looks like something I’d push for using in the team(s) I’ll be working with.

Though I’d probably only check it out after invariants are added. They complete the picture.

Agreed on both points. This looks very useful already, but invariants would be a very welcome addition.

I’m working through some ideas that I have for adding invariants to Bond.

The challenge is that invariants as used in object-oriented languages (such as Eiffel, where DbC was originally conceived) are embedded in class definitions and the assertions therein have access to the state of the “current” object (Current in Eiffel, this or self in some other OO languages).

In a functional language such as Elixir, we don’t have stateful “objects” that the assertions in invariants could refer to. What kind of invariants could you define for a purely functional Stack module, for example, without having a reference to the “current” stack?

On the other hand, Elixir does have some near analogues in the form of stateful processes, such as Agents and GenServers. I think it could be possible to use the pid of the process as the notion of “current” for use in invariants, and “tap into” the state of these processes for making assertions about the state.

This approach would likely require wrapper modules around Agent and/or GenServer in order to be able to pass the “current state” to assertions in a hypothetical @invariant clause.

I’m still thinking through these ideas, though, and I am definitely open to feedback or alternative approaches to adding invariants to Bond.

Invariants on function arguments only?

I think you should completely do away with stateful assertions, be those pre-conditions, post-conditions or invariants. Up to you of course but that’s IMO having the potential to become a huge mess and a maintenance nightmare.

Thanks for the feedback @dimitarvp.

You might be right about stateful assertions becoming messy. I had been thinking about invariants as inherently stateful, and which describe properties of the state before and after state transitions. But as you point out, there is probably still value in stateless invariants that use only function arguments.

For example, consider a bounded stack with a capacity fixed at creation time. Such stacks do not allow new items to be pushed if the stack is already full. I can think of a few invariants that I would express at the module level, even for a purely functional, stateless version of such a stack (ignore for now how the stack variable binding could be injected into the assertions, I’ll come back to that):

@invariant size_limited_by_capacity: size(stack) <= capacity(stack),
           non_negative_size: size(stack) >= 0,
           fixed_capacity: capacity(stack) == old(capacity(stack)),
           full_implies_at_capacity: full?(stack) ~> (size(stack) == capacity(stack))

Many of these invariant properties could be expressed as postconditions on the relevant functions, but expressing them at the module level as invariants brings to mind a couple of possible advantages:

  1. The invariants could be checked at run-time before and after every function call.
  2. The invariants could be added to the @moduledoc in a similar way that preconditions and postconditions are already added to the @doc for functions.

The main complication that I can think of is that this scheme would probably only work for 1-arity functions that use the same name for the lone parameter. Otherwise, what would be the value bound to the stack variable in the invariant assertions?

I’m also not sure if the old expression in the fixed_capacity assertion in the invariant makes sense. If invariants are to be checked before and after function calls, the old expression would fail when evaluated before the function call (at least the way that old is currently implemented in Bond). I don’t think Eiffel allows old to be used in invariants, presumably for this reason.

Curious about your thoughts, or if you (or anyone else) have other ideas about invariants for purely functional code.

1 Like

I added a new “Contracts in a Concurrent World” guide to the Bond docs, which discusses how to eliminate the need for stateful assertions:

https://hexdocs.pm/bond/contracts-and-concurrency.html

TL;DR - It’s the same old trick used for better testability: separate the pure functional code from stateful code.

1 Like

A few thoughts about module-level invariants.

Invariants come in two flavors: those that desugar into pre- and post-conditions (ensure invariant holds before and after), and those that desugar into only post-conditions (ensure something holds between the original and new value).

Invariants also need some way to be applied when functions return a wrapped value. Consider your bounded stack – a push operation would definitely want the size_limited_by_capacity invariant checked, but it would also likely return {:ok, stack} | :error.

Some hypothetical syntax, adapting your above stack example:

@invariant size_limited_by_capacity(stack) :: size(stack) <= capacity(stack)
@invariant fixed_capacity(stack) :: new_stack :: capacity(stack) == capacity(new_stack)
defstruct [...]

@invariants pre: stack, post: {:ok, stack} :: stack
def push(%BoundedStack{} = stack, element) do
  ...
end

This would convey that, prior to the function running, the stack is accessed as stack (any variable bound in the params), and after the function runs, the stack is accessed only if it matches {:ok, stack}, in which case stack is used.

1 Like

This is a very well made doc page, thanks for putting it in.

In my case I’d use your library to (1) check function arguments and (2) check for various invariants of the values assigned to variables after calling 3rd party APIs, and just any intermediate state really (local variables). For this, stateless assertions are more than enough.

You’ve done a good job isolating the stateful component in the page above and you also stated the limitations. IMO that’s good enough or else we’ll have to all start coding in TLA+ (or Wasm’s WIT).

At least my idea for contract-driven programming in a language with strong but dynamic typing is basically: manage expectations; make them explicit. Which is part of my bigger philosophy that all code should be declarative (and at least on my part this is why I like FP much more; I write Enum.each or Enum.map to express what I want done, not do cryptic for loops in a C-derived language to always show how I do the thing and then maybe the reader will manage to intuit the “how”).

So I am not sure I am the right person to ask for feedback as my general idea is to declare expectations in code and have as many of them as possible, which opens the doors for actually intelligent tooling in the future which can run tests for us, see a problem and start testing all assertions in the contract and eventually find which one has failed and then it’d be able to tell you “Seems like your mock of this 3rd party API is not returning what you expect it to; you should modify it like this or that”.

For that to happen, we need our code to be of the type “We do X and we expect A, B, C before, and D, E, F after”. And now we’re venturing in the territory of Ada, but at least our compiler and tooling are not paid. :smiley:

1 Like

Hmm . can this be used to add pre and post conditions for context functions calling out to Ecto in phoenix ? I mean often you send an id and some map to update a specific object in the database. By using pre and post (and maybe old, but not in this example), we can maybe do something ala

  @pre attrs_doesnt_have_id: not Map.has_key?(attrs, :uuid) # doesnt make sense and elixir without specs littered everywhere allows for it
  @post is_user: is_struct(result, User),
        all_fields_updated: Enum.all?(attrs, fn {key, value} -> Map.get(result, key) == value end)
  def update_user(%User{uuid: uuid}, attrs) do
    # ....
  end

? :slight_smile: Its basically a runtime test. a contrived example because result in this case will be {:ok, result}

could maybe also just use old and compare the result to the old result, that its different … but that wont check individual fields ofc

1 Like

fun :slight_smile: <3

  @post is_hallo: result == :hallo
  def hello do
    :world
  end

in this case dialyzer is screaming at me already … but its MUCH easier to actually get the error in your face … than dialyzer warning about something that SHOULD fail … but never does. ref this thread where dialyzer warns about something that never fails Dialyzer warning from hell: no_return when calling erl_tar.create - #2 by jarlah

iex(1)> TestBond.hello()
** (Bond.PostconditionError) postcondition failed in TestBond.hello/0
|   label: :is_hallo
|   assertion: result == :hallo
|   binding: [result: :world]

    (test_bond 0.1.0) lib/test_bond.ex:6: TestBond.hello/0
    iex:1: (file)
iex(1)> 

its probably more valuable in the ecto example i described above

2 Likes

Hmm . can this be used to add pre and post conditions for context functions calling out to Ecto in phoenix ? I mean often you send an id and some map to update a specific object in the database. By using pre and post (and maybe old, but not in this example)

Yes, that is precisely the kind of thing that Bond (and Design by Contract in general) was designed for.

Note that there is no need for old expressions when your assertions are working with stateless code. If you can write your assertions using only the values for the arguments to the function and the special result variable that is available in postconditions, then you don’t need old at all.

The only thing I’d add with regard to your example is that the all_fields_updated assertion in your postcondition doesn’t lend itself to good error reports if the assertion fails. Using Enum.all?/2 is perfectly valid in assertions, but since it just returns false if any element in the enumerable doesn’t match expectations, you won’t be able to tell which field/value caused it to fail.

It might be better to use a dedicated function for this particular assertion, maybe something like this (untested, but just to give an idea):

defp all_fields_match?(struct, attrs) do
  Enum.all?(attrs, fn {key, expected_value} ->
    actual_value = Map.get(struct, key)
    check(
      actual_value == expected_value,
      "expected value for #{key} to equal #{expected_value}, got #{actual_value}")
  end)
end

If you take this approach, the all_fields_match?/2 function could also convert between string keys and atom keys, as necessary, and also coerce values that have different types in the attrs map vs the Ecto schema struct.

Invariants also need some way to be applied when functions return a wrapped value. Consider your bounded stack – a push operation would definitely want the size_limited_by_capacity invariant checked, but it would also likely return {:ok, stack} | :error .

This would convey that, prior to the function running, the stack is accessed as stack (any variable bound in the params), and after the function runs, the stack is accessed only if it matches {:ok, stack} , in which case stack is used.

Very interesting ideas, @zachallaun. I don’t think I can get that exact syntax to work in Bond, but what has become clear to me by your examples is that invariant checking at run-time probably needs to be “opt-in” on a per function basis. You’ve hypothesized an additional @invariants attribute for this purpose, which would allow functions to bind variables to be passed to the @invariant and for pattern matching and/or unwrapping the result from functions. I think this idea has a lot of merit, and I’ll think about how this could be applied in Bond to add support for invariants.

Thank you

1 Like

Hi, good library, I’ve read the code and while I found idea of contract programming very interesting, but I have some question about the implementation:

  1. Why do you override the def, defp and @ functions? It makes this library inapplicable with other libraries (like decorators, for example). More traditional approach is to use @on_definition callback to collect data for each function and then @before_compile to replace implementations of the functions. This way it is compatible with other solutions.
  2. Why do you use gen_statem? Module is always compiled in a single process.
  3. Bond.FunctionWithContract.function_id will fail when context atom in variable is not nil (for example code was generated by macro)
  4. It tries to insert assertions to every clause, which results in code failing to compile with cryptic error when assertion references a variable which is present only in one clause. I think that this is a problem with the design of the solution, not with the implementation. Is it expected?
  5. Predicates work not only with booleans, but their spec states otherwise. Why?

Thank you for the feedback, @Asd. I’ve attempted to answer all of your questions below.

Why do you override the def, defp and @ functions? It makes this library inapplicable with other libraries (like decorators, for example). More traditional approach is to use @on_definition callback to collect data for each function and then @before_compile to replace implementations of the functions. This way it is compatible with other solutions.

As mentioned in the history section of the Bond docs the implementation of Bond is based on an older contracts library, ex_contract, from Dariusz Gawdzik. I carried over some of the code from ex_contract more or less directly.

However, you make a good point about compatibility with other libraries, so I will revisit the implementation and try to use @on_definition and @before_compile instead of overriding various Kernel macros.

Why do you use gen_statem? Module is always compiled in a single process.

I chose to use a finite state machine for keeping track of compile state. I chose gen_statem simply because it is already available with Erlang and I didn’t have to pull in an extra dependency for an FSM.

Bond.FunctionWithContract.function_id will fail when context atom in variable is not nil (for example code was generated by macro)

I will look into this and commit a fix.

It tries to insert assertions to every clause, which results in code failing to compile with cryptic error when assertion references a variable which is present only in one clause. I think that this is a problem with the design of the solution, not with the implementation. Is it expected?

This is an intentional design decision: to have preconditions and postconditions defined before the first clause of a function, and apply those preconditions and postconditions to every clause of that function.

Not everyone agrees with that design decision, though, as can be witnessed in the discussion on my unmerged pull request for ex_contract.

My opinion, informed by Bertrand Meyer’s writing on Design by Contract, and especially Object-Oriented Software Construction, is that contracts are part of the public interface for a module and its functions, and not simply an implementation aid to the developer of a module. To me this means that contracts should be declarative and specify the observable aspects of a function.

In the case of multi-clause functions, it is an implementation detail to use different names for parameters in the different clauses of the function, and that implementation detail is not even visible to callers of the function unless they look directly at the source code. I.e., it’s not in the docs and not part of the public interface for the function.

That said, I do think I could make improvements to Bond to make it easier to define contracts for multi-clause functions. I’m thinking of adding some sort of bind clause to assertions in Bond, which would allow for pattern matching on arguments and binding arguments to arbitrary names. (Incidentally, this might also help with defining invariants at the module level by providing a mechanism for invariants to reference function parameters and/or pattern match on function results, as discussed with @zachallaun above.)

In the meantime, the best approach is just to use consistent names for parameters in all clauses of a multi-clause function. If the generic name for a parameter is not sufficient in the context of the individual function clause, then an alias could be used. Something like the following, perhaps (untested):

@spec get(URI.t() | String.t()) :: term()
@pre uri_string_or_struct: is_binary(uri) or is_struct(uri, URI),
     uri_string_is_parseable: is_binary(uri) ~> URI.parse(uri)
def get(%URI{} = uri) do
  http_request(uri)
end

def get(uri = url_string) when is_binary(url_string) do
  get(URI.parse(url_string)
end

Note the alias of the uri parameter as url_string in the second clause of the get/1 function, which allows the generic name uri to be used in the contract but still allows for a more meaningful name for that specific function clause.

Predicates work not only with booleans, but their spec states otherwise. Why?

This was simply an oversight on my part. I’ve updated the specs to look like this instead:

@spec xor(as_boolean(term()), as_boolean(term())) :: boolean()
@spec implies?(as_boolean(term()), as_boolean(term())) :: boolean()

This will be in the next release of Bond.

1 Like