Zenn
Open2

PropCheckでステートフルプロパティテスト

Elixir
Test
#
propcheck
sankakusankaku
  • テスト対象が純粋関数の場合、返ってきた新しい状態を扱えない。そのため GenServer とかでテスト対象をくるむ必要がある。
  • それに対し、モデル側は純粋じゃないといけない感じ。
    • postcondition に入ってくる state がコマンドによって更新されるまえの状態なので、next_state とは別に更新後の状態を得る必要があるので。
defmodule Els.JustMap do
  defstruct map: %{}

  def new() do
    %__MODULE__{map: %{}}
  end

  def put(%__MODULE__{map: map} = jm, k, v) do
    %__MODULE__{jm | map: Map.put(map, k, v)}
  end

  def fetch(%__MODULE__{map: map} = _jm, k) do
    Map.fetch(map, k)
  end

  def delete(%__MODULE__{map: map} = jm, k) do
    %__MODULE__{jm | map: Map.delete(map, k)}
  end

  def pop(%__MODULE__{map: map} = jm, k) do
    {v, map} = Map.pop(map, k)
    {v, %__MODULE__{jm | map: map}}
  end
end

defmodule Els.JustMapServer do
  use GenServer
  alias Els.JustMap

  def start_link() do
    GenServer.start_link(__MODULE__, JustMap.new(), name: __MODULE__)
  end

  def init(init_arg) do
    {:ok, init_arg}
  end

  def stop() do
    GenServer.stop(__MODULE__)
  end

  def put(k, v) do
    GenServer.cast(__MODULE__, {:put, k, v})
  end

  def fetch(k) do
    GenServer.call(__MODULE__, {:fetch, k})
  end

  def delete(k) do
    GenServer.cast(__MODULE__, {:delete, k})
  end

  def pop(k) do
    GenServer.call(__MODULE__, {:pop, k})
  end

  def handle_cast({:put, k, v}, jm) do
    {:noreply, JustMap.put(jm, k, v)}
  end

  def handle_cast({:delete, k}, jm) do
    {:noreply, JustMap.delete(jm, k)}
  end

  def handle_call({:fetch, k}, _from, jm) do
    {:reply, JustMap.fetch(jm, k), jm}
  end

  def handle_call({:pop, k}, _from, jm) do
    {v, jm} = JustMap.pop(jm, k)
    {:reply, v, jm}
  end
end

defmodule Els.JustMapModel do
  defstruct map: %{}

  def new() do
    %__MODULE__{map: %{}}
  end

  def put(%__MODULE__{map: map} = jm, k, v) do
    %__MODULE__{jm | map: Map.put(map, k, v)}
  end

  def fetch(%__MODULE__{map: map} = _jm, k) do
    Map.fetch(map, k)
  end

  def delete(%__MODULE__{map: map} = jm, k) do
    %__MODULE__{jm | map: Map.delete(map, k)}
  end

  def pop(%__MODULE__{map: map} = jm, k) do
    {v, map} = Map.pop(map, k)
    {v, %__MODULE__{jm | map: map}}
  end
end

defmodule Els.JustMapTest do
  use ExUnit.Case
  use Els.PropCheck
  use PropCheck.StateM
  import Mox

  setup :verify_on_exit!

  alias Els.JustMapModel
  alias Els.JustMapServer

  property "JustMap state-full property", [:verbose] do
    forall cmds <- commands(__MODULE__) do
      {:ok, _pid} = JustMapServer.start_link()
      {history, state, result} = run_commands(__MODULE__, cmds)
      JustMapServer.stop()

      (result == :ok)
      |> when_fail(
        IO.puts("""
        history: #{inspect(history)}
        state: #{inspect(state)}
        result: #{inspect(result)}
        """)
      )
    end
  end

  @impl true
  def initial_state() do
    JustMapModel.new()
  end

  @impl true
  def command(state) do
    oneof([
      {:call, JustMapServer, :put, [gen_key(state), term()]},
      {:call, JustMapServer, :fetch, [gen_key(state)]},
      {:call, JustMapServer, :delete, [gen_key(state)]},
      {:call, JustMapServer, :pop, [gen_key(state)]}
    ])
  end

  def gen_key(%JustMapModel{map: map}) do
    oneof([oneof([Map.keys(map)]), utf8()])
  end

  @impl true
  def precondition(%JustMapModel{}, _) do
    true
  end

  @impl true
  def next_state(%JustMapModel{} = state, _res, {:call, JustMapServer, :put, [k, v]}) do
    JustMapModel.put(state, k, v)
  end

  @impl true
  def next_state(%JustMapModel{} = state, _res, {:call, JustMapServer, :delete, [k]}) do
    JustMapModel.delete(state, k)
  end

  @impl true
  def next_state(%JustMapModel{} = state, _res, {:call, JustMapServer, :fetch, [_k]}) do
    state
  end

  @impl true
  def next_state(%JustMapModel{} = state, _res, {:call, JustMapServer, :pop, [k]}) do
    {_, new_state} = JustMapModel.pop(state, k)
    new_state
  end

  @impl true
  def postcondition(%JustMapModel{} = state, {:call, JustMapServer, :fetch, [k]}, res) do
    res == JustMapModel.fetch(state, k)
  end

  @impl true
  def postcondition(%JustMapModel{} = state, {:call, JustMapServer, :pop, [k]}, res) do
    {val, _new_state} = JustMapModel.pop(state, k)
    res == val
  end

  @impl true
  def postcondition(%JustMapModel{} = _state, _, _res) do
    true
  end
end
sankakusankaku

検査対象のサーバは以下のようなやり方で簡単に書けるんじゃないだろうか？
実行速度は悪くなるかもしれない。

defmodule Els.JustMapServer do
  use GenServer
  alias Els.JustMap

  def start_link() do
    GenServer.start_link(__MODULE__, JustMap.new(), name: __MODULE__)
  end

  def init(init_arg) do
    {:ok, init_arg}
  end

  def stop() do
    GenServer.stop(__MODULE__)
  end

  def put(k, v) do
    fn state ->
      {:noreply, :ok, JustMap.put(state, k, v)}
    end
    |> call_fun()
  end

  def fetch(k) do
    fn state ->
      {:noreply, JustMap.fetch(state, k), state}
    end
    |> call_fun()
  end

  def delete(k) do
    fn state ->
      {:noreply, :ok, JustMap.delete(state, k)}
    end
    |> call_fun()
  end

  def pop(k) do
    fn state ->
      {v, state} = JustMap.pop(state, k)
      {:reply, v, state}
    end
    |> call_fun()
  end

  defp call_fun(fun) do
    GenServer.call(__MODULE__, {:call_fun, fun})
  end

  def handle_call({:call_fun, fun}, _from, state) do
    fun.(state)
  end
end