前提条件

コンピュータプログラミングにおいて、前提条件とは、コードの一部を実行する直前、または正式な仕様での操作の前に常に真でなければならない条件または述語です。

前提条件に違反すると、コードセクションの効果は未定義になり、意図した動作が実行されない可能性があります。前提条件が欠落している、不十分である、または正式に証明されていない (または証明の試みが間違っている)、あるいは静的または動的にチェックされていないと、特に厳密に型指定されていない安全でない言語では、セキュリティの問題が発生する可能性があります。

多くの場合、前提条件は影響を受けるコード セクションのドキュメントに単に組み込まれます。前提条件は、コード自体内のガードまたはアサーションを使用してテストされることがあり、一部の言語には、これを行うための特定の構文構造があります。

階乗関数は、そのパラメータが 0 以上の整数である場合にのみ定義されます。したがって、階乗関数の実装には、そのパラメータが整数であり、パラメータが 0 以上であるという前提条件があります。あるいは、言語の型システムを使用して、階乗関数のパラメータが自然数 (符号なし整数) であることを指定することもできます。これは、コンパイラの型チェッカーによって自動的に形式的に検証できます。

さらに、数値型の範囲が限られている場合 (ほとんどのプログラミング言語と同様)、オーバーフローが発生しないようにするには、前提条件でパラメーターが持つことができる最大値も指定する必要があります。 (例: factorial の実装が結果を 64 ビットの符号なし整数で返す場合、factorial(21) は 64 ビットで格納できる最大の符号なし整数より大きいため、パラメーターは 21 未満でなければなりません)。言語が範囲サブタイプをサポートしている場合 (例: Ada )、このような制約は型システムによって自動的に検証できます。より複雑な制約は、証明支援機能を使用して対話的に形式的に検証できます。

オブジェクト指向ソフトウェア開発における前提条件は、契約による設計の重要な部分です。契約による設計には、事後条件とクラス不変の概念も含まれます。

あらゆるルーチンの前提条件は、正常に実行するために必要なオブジェクトの状態に対する制約を定義します。プログラム開発者の観点から見ると、これはルーチン呼び出し側の契約部分を構成します。呼び出し側は、ルーチンを呼び出す前に前提条件が満たされていることを確認する義務があります。呼び出し側の努力に対する報酬は、呼び出されたルーチンの事後条件で表現されます。^[1]

Eiffelで記述された次の例のルーチンは、1 日の 1 時間に有効な値 (0 から 23 まで) である整数を引数として受け取ります。前提条件はキーワード に続きますrequire。これは、引数が 0 以上 23 以下でなければならないことを指定します。タグ " valid_argument:" はこの前提条件句を説明し、実行時に前提条件違反が発生した場合にこれを識別するために役立ちます。

    set_hour ( a_hour : INTEGER ) -- `hour' を `a_hour' に設定する有効な引数が必要: 0 <= a_hourかつa_hour <= 23であるhour := a_hourであることを確認するhour_set : hour = a_hourであることを確認するend  
            
        
                   
        
              
        
               
        

継承が存在する場合、子孫クラス (サブクラス) に継承されたルーチンは、その前提条件が有効な状態で実行されます。つまり、継承されたルーチンの実装または再定義も、継承された契約に準拠するように記述する必要があります。再定義されたルーチンでは前提条件を変更できますが、弱めることはできます。^[2]つまり、再定義されたルーチンはクライアントの義務を軽減することはできますが、増やすことはできません。

• 契約による設計
• ガード（コンピュータサイエンス）
• 事後条件
• ホーア論理
• 条件によって維持される不変量
• データベーストリガー