コントラクト

コントラクトでは以下の制御構文を用いる。

これらの制御構文は擬似引数解決ディレクティブである。

contract require precondition 擬似引数解決ディレクティブ

contract require precondition 擬似引数解決ディレクティブは引数 if, group, message を取る。if 引数は必須であり、group 引数と message 引数は省略可能である。message 引数はリテラルな文字列である必要がある。

引数解決の試行が行われたとき、まず group 引数が計算される。引数解決ディレクティブのヒエラルキーによって contract require precondition 擬似引数解決ディレクティブが有効と判断されれば、続いて if 引数が計算される。if 引数の値が真であり、なおかつ contract not require precondition 擬似引数解決ディレクティブによって無効化されなければ、contract require precondition 擬似引数解決ディレクティブは有効である。引数解決の試行で、有効な contract require precondition 擬似引数解決ディレクティブが存在するにもかかわらず、有効な contract precondition 擬似引数解決ディレクティブが存在しなければ、インタープリターを停止する。このとき、contract require precondition 擬似引数解決ディレクティブの message 引数がエラーメッセージとして使用される。

contract precondition 擬似引数解決ディレクティブ

contract precondition 擬似引数解決ディレクティブは引数 if, group, message を取る。if 引数は必須であり、group 引数と message 引数は省略可能である。message 引数はリテラルな文字列である必要がある。

引数解決の試行が行われたとき、まず group 引数が計算される。引数解決ディレクティブのヒエラルキーによって contract precondition 擬似引数解決ディレクティブが有効と判断されれば、続いて if 引数が計算される。if 引数の値が真であり、なおかつ contract omit precondition 擬似引数解決ディレクティブによって無効化されなければ、contract precondition 擬似引数解決ディレクティブは有効である。引数解決の試行で、有効な contract precondition 擬似引数解決ディレクティブが存在するにもかかわらず、その引数解決の終端要因がブーリアン型の false へのフォールバックであれば、インタープリターを停止する。このとき、contract precondition 擬似引数解決ディレクティブの message 引数がエラーメッセージとして使用される。

contract postcondition 擬似引数解決ディレクティブ

contract postcondition 擬似引数解決ディレクティブは引数 if, then, group, message を取る。if 引数と then 引数は必須であり、group 引数と message 引数は省略可能である。message 引数はリテラルな文字列である必要がある。

引数解決の試行が行われたとき、まず group 引数が計算される。引数解決ディレクティブのヒエラルキーによって contract postcondition 擬似引数解決ディレクティブが有効と判断されれば、続いて if 引数が計算される。if 引数の値が真であり、なおかつ contract omit postcondition 擬似引数解決ディレクティブによって無効化されなければ、contract postcondition 擬似引数解決ディレクティブは有効である。

引数解決の対象となる統合演算式の実行が終了すると、その引数解決で有効とされた contract postcondition 擬似引数解決ディレクティブの then 引数が計算される。そして、いずれかの then 引数の値が偽であれば、インタープリターを停止する。このとき、contract postcondition 擬似引数解決ディレクティブの message 引数をエラーメッセージとして用いる。引数解決の対象となる統合演算式が終了せずに中断された場合には、contract postcondition 擬似引数解決ディレクティブの then 引数は計算されない。halt プリミティブ演算でインタープリターを停止した場合、コンティニュエーションを実行して現在の動的環境を破棄した場合などが、これに該当する。

contract not require precondition, contract omit precondition, contract omit postcondition 擬似引数解決ディレクティブ

contract not require precondition, contract omit precondition, contract omit postcondition 擬似引数解決ディレクティブは、それぞれ if 引数と group 引数を取る。if 引数は必須であり、group 引数は省略可能である。

引数解決の試行が行われたとき、まず group 引数が計算される。引数解決ディレクティブのヒエラルキーによって、これらの擬似引数解決ディレクティブが有効と判断されれば、続いて if 引数が計算される。if 引数の値が真であれば、自分自身よりも前方に記述されている、対応する擬似引数解決ディレクティブを無効化する。対応する擬似引数解決ディレクティブとは、contract not require precondition, contract omit precondition, contract omit postcondition に対して、それぞれ contract require precondition, contract precondition, contract postcondition である。

引数解決ディレクティブのヒエラルキー

コントラクトを構成する 6 種類の擬似引数解決ディレクティブは、すべて引数解決ディレクティブのヒエラルキーの対象になる。これらの擬似引数解決ディレクティブの group 引数と message 引数を計算する過程では、すべての引数解決ディレクティブが無効である。group 引数を省略すると、その擬似引数解決ディレクティブは contractmain グループに属する。if 引数と then 引数を計算する過程では、引数解決ディレクティブのヒエラルキーが適用される。

コントラクトで使用できる引数

コントラクトを構成する擬似引数解決ディレクティブの引数のうち、if 引数を事前条件 (precondition)、then 引数を事後条件 (postcondition) という。

事前条件を計算する過程では、他の引数解決ディレクティブと同様に、コンテキスト引数と引数解決時引数を使用できる。

事後条件を計算する過程では、コンテキスト引数は使用できるが、引数解決時引数を使用できない。かわりに、事後条件では事後条件引数 (postcondition argument) を使用できる。varb 事後条件引数の値は、引数解決の試行の時点での演算指定子の値である。引数解決の試行の時点での統合演算式の引数の値は、同名の事後条件引数で得られる。return value 事後条件引数の値は、引数解決の対象となった統合演算式の戻り値の値である。これらに該当しない事後条件引数の値はブーリアン型の false である。

アサーション

コントラクトが擬似引数解決ディレクティブであるのに対して、アサーションはプリミティブ演算である。

assert プリミティブ演算は main 引数と message 引数を取る。main 引数の値が偽であるとき、インタープリターを停止する。このとき message 引数の値をエラーメッセージとして用いる。

実装による選択

実装によってはコントラクトとアサーションを処理しないことがある。また、実装によっては、コントラクトまたはアサーションに違反してもインタープリターを停止せず、単にログに記録するだけである場合がある。インタープリターを停止することがフェイルセーフでない動作環境においては、このような実装を選択すべきである。