Flat Leon Works

アプリやゲームを作ってます。

【Nim】お手軽契約プログラミング

この記事は「Nim Advent Calendar 2021」の25日目の記事として登録させてもらっています。

契約プログラミングとは

契約プログラミング - Wikipedia

契約プログラミングとは、関数やクラスに対して予め条件を設定し、それを利用者と実装者双方で条件を守るようにする(つまり契約する)プログラミング手法です。契約プログラミングを行うことで、関数やクラスの実装者は何を実装すべきかが明確になり、またその利用者はその関数やクラスの挙動が明確になるというメリットがあります。

契約プログラミングで利用される条件は以下の3つです。

  • 事前条件 : 関数に対して設定
  • 事後条件 : 関数に対して設定
  • 不変条件 : クラスに対して設定

条件は1つだけではなく、何個でも設定することが可能です。

事前条件

事前条件は関数に対して設定されるものです。事前条件は関数を呼び出す前(正確には関数開始時)の条件です。例えば、文字列を数値に変換する関数は事前条件として「引数の文字列には数字のみ含まれる」という条件を設定したりします。 事前条件は関数の利用者が守るべきルールです。事前条件に違反した関数呼び出しに対して関数はその役割を果たす必要はありません。 事前条件として設定できるのは引数だけでなくなんでもよいです。例えば、「ネットワークに接続されている」などでも構いません。

事後条件

事後条件は関数が呼び出された直後の条件です。例えば、文字列を数値に変換する関数は事後条件として「0以上の数値を返す」という条件を設定したりします。 事後条件は関数の実装者が守るべきルールです。関数が事後条件に違反している場合は、その関数にバグがあるということになります。 事後条件として設定できるのは戻り値だけでなくなんでもよいです。例えば、「hogeと標準出力する」などでも構いません。

不変条件

不変条件はどんなときでも変わらない条件です。例えば人間クラス(Human)の変数に年齢(age)があったとして、人間クラスの不変条件として、「ageは0以上」という条件を設定したりします。 ageを変更する者はこの条件を常に守る必要があります。またageを利用する者はこの条件を前提にすることができます。

Nimで(お手軽)契約プログラミング

契約プログラミング自体は、実装者と利用者の間の約束ごとであり、ドキュメント上だけで完結させることもできます。 しかし、条件のチェックを処理に組み込んでおくことでより確実に契約プログラミングを遵守させることができます。

それをNimで行う方法を紹介したいと思います。ただし、お手軽版なので、「事前条件」と「事後条件」のみで、「不変条件」は扱いません。

事前条件をチェックする

事前条件は、関数開始時の条件です。つまり、関数の実装の最初に条件をチェックすればいいだけです。

文字列を数値に変換する関数の事前条件のチェックは以下のようにします。

proc stringToInt( x: string ): int
  # 事前条件 : 引数に含まれる文字は数字のみ
  when compileOption("assertions"):
    for c in x:
      if not c.isDigit: assert( false, "pre condition failed" )
  〜実装〜

条件のチェックといえば、assertです。また、事前条件はassertが有効になっている場合のみ行いたいので、when compileOption("assertions"):assertが有効になっているかどうかをチェックしています。

事後条件をチェックする

事後条件は、関数終了時の条件です。関数の終了時の処理は関数の末尾で行えばよいというわけではありません。関数の途中でreturnされる可能性があるためです。また、戻り値もチェックできるようにしたいです。幸い、Nimにはdeferという事後条件チェックに最適な言語機能があります。

文字列を数値に変換する関数の事後条件のチェックは以下のようにします。

proc stringToInt( x: string ): int
  # 事前条件 : 戻り値は0以上
  when compileOption("assertions"):
    defer:
      assert( result >= 0, "post condition failed" )
  〜実装〜

deferを使うことで、関数の途中のreturnも、戻り値のチェックもできます。ちなみに、result変数を使わず直接returnした場合もdeferではresultに戻り値が格納されるようです。まじ便利。

pre/postで記述できるようにする

事前条件/事後条件のチェック処理を以下のようにpre/postテンプレート化しておくと、もっと楽に記述できるようになります。

template pre( x: untyped ): untyped =
  when compileOption("assertions"):
    if not x:
      echo "===== pre condition failed ====="
      assert( false )
template post( x: untyped ): untyped =
  when compileOption("assertions"):
    defer:
      if not x:
        echo "===== post condition failed ====="
        assert( false )

使い方

proc stringToInt( x: string ): int
  pre:
    var check = true
    for c in x:
      if not c.isDigit:
        check = false
        break
    check
  post:
    result >= 0

  〜実装〜

各pre/postブロック内の最後の式の真偽値が条件の合否になります。*1

Nimの契約プログラミングライブラリ

非公式ですが契約プログラミングに関するNimのライブラリがいくつかあるようです。もっと真面目に契約プログラミングを行いたい場合は、これらを利用を検討してください。

*1:Nimの挙動的にこれが正式なものなのかわかりませんが、とりあえず動くようです。ちなみに、block節を式で使うと、最後の式が評価結果になるのはマニュアルに書いてあります。