自動ソフトウェア検証の要件を調べています。つまり、コード（CやJavaなどの言語で記述された通常の手続き型コード）を取り込むプログラムは、各ループを最終的に停止する必要があり、アサーションに違反しないという一連の定理を生成します。 、nullポインターなどの逆参照は決してありません。次に、それが実際に真であることを証明するために定理証明者に渡します（または、コードのバグを示す反例を見つけます）。
問題は、どのようなロジックを使用するかです。2つの主要な位置は次のようです。
一階述語論理は問題ありません。
一階述語論理は十分に表現力がありません。高階述語論理が必要です。
問題は、両方のポジションに多くのサポートがあるようだということです。では、どちらが正しいのでしょうか。それが2番目の場合、一階述語論理に基づくベリファイアで問題が発生する、実行したいことの利用可能な例はありますか？
FOLで必要なことはすべて行うことができますが、それは多くの余分な作業です-たくさん！既存のシステムのほとんどは、時間や労力を節約するために学者や人々によって開発されたものであるため、時間や労力を節約するためにショートカットを使用するように誘惑され、HOLや関数型言語などに惹かれます。数百人ではなく、数十万人が使用するシステムであるFOLは、より多くのユーザーが利用しやすいため、進むべき道であると考えています。仕事をすることに代わるものはありません。私たちは25年前からこれに取り組んできました！私たちのプロジェクトを見てください（http://www.manmademinions.com）
よろしく、アーロン。
私の実務経験では、「1.一階論理で十分」のようです。一次論理に基づく仕様言語で完全に記述されたさまざまな関数の完全な仕様の例については、例としてACSL by Exampleまたはこのケース スタディを参照してください。
一階論理には、プログラム検証から得られる適切なプロパティを処理するために長年にわたって改良されてきた自動証明器 (証明アシスタントではない) があります。これらの使用のための注目すべき自動証明は、たとえばSimplify、Z3、およびAlt-ergoです。これらの証明者が失敗し、それらを助けるために追加できる明らかなレンマ/アサーションがない場合でも、困難な証明義務のために証明アシスタントを起動する手段があります。逆にHOLを使うと、SimplifyもZ3もAlt-ergoも全く使えないし、高階論理の自動証明器は聞いたことはあるが、プロパティに関しては効率がいいと褒められた話は聞いたことがないプログラムから。
FOL はほとんどの検証条件に適していますが、コレクション内の要素の合計に関するプロパティを証明する場合など、少数の場合は高次のロジックが非常に重要であることがわかりました。したがって、私たちの定理証明器 (Perfect Developer と Escher C Verifier で使用される) は基本的に一次ですが、高次の推論も行うことができます。