Hoare

Declared state transitions as pre/post contracts.

A transition names the states it leaves and the state it reaches, the guards that must hold, and the effects it performs on the way. {from, guards} body {to} is a Hoare triple; Hoare.Transition.run/4 discharges it and keeps one law: a run ends in to or leaves the record in from, never between.

check   from ▸ guards            pure, on the resolved record
perform effects                  IO; bare = idempotent, {run, undo} = reverted on failure
commit  lock ▸ re-read ▸ body ▸ write to ▸ assert to     one transaction

Installation

def deps do
  [
    {:hoare, "~> 0.1"}
  ]
end

States

A state is a module: the status that tags a record, the reason when it does not, and the properties that refine the tag and extract witnesses.

defmodule PendingUnpack do
  @behaviour Hoare.State
  defstruct [:record, :package]

  def status, do: :PENDING_UNPACK
  def missing, do: :not_pending_unpack
  def properties, do: [&single_package/1]

  defp single_package(%{record: %{packages: [package]}} = state), do: {:ok, %{state | package: package}}
  defp single_package(%{record: %{packages: []}}), do: {:error, :no_packages}
  defp single_package(_), do: {:error, :multiple_packages}
end

Hoare.State.match/2 builds the struct or says why the record is not in that state. A state entered by one transition is the same module another leaves from, so the graph is nominal and inspectable.

Transitions

defmodule Repack do
  defstruct [:record, :state, :label]

  def transition do
    %Hoare.Transition{
      from: [PendingUnpack],
      to: Packed,
      effects: [{&purchase_label/1, &release_label/1}]
    }
  end

  defp purchase_label(ctx), do: with({:ok, label} <- Carrier.buy(ctx.state.package), do: {:ok, %{ctx | label: label}})
  defp release_label(%{label: label}), do: :ok = Carrier.release(label)
end

The context is any struct with record and state keys. The module owning the records supplies the body of the commit and the store:

Hoare.Transition.run(Repack.transition(), %Repack{record: order}, &write_package/1, store: Repo)
# {:ok, %Repack{record: %Order{status: :PACKED}, ...}} | {:error, reason}

commit/5 takes the store's lock on {schema, id} (or opts[:lock]), re-reads the record and refuses it unless still tagged by a from state, runs the body, writes to's status through the schema's changeset/2, and asserts to before the transaction closes. A record already in to is a concurrent run: it converges as {:ok, record} when every completed effect was bare, and is {:error, :status_changed} when one must be undone.

Store

Hoare.Store is the three operations the commit needs: transact_with_lock/2, fetch/2, update/1. An Ecto repo supplies the last as is and declares the other two.

Results

Hoare.Result holds the few combinators the runner is built from: bind/2, kleisli/1, tap_ok/2, tap_error/2, map_error/2. Tagged tuples throughout; nothing is wrapped.