Bond - Design by Contract for Elixir

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.

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.

@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.

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

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

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.