しばらく検索しましたが、「述語検査」で簡潔な定義を見つけることができません。いつ述語チェックを適用できますか？ホアレのトリプルとどう違うの？ Hoareのトリプルをすべてのコード行に正しく適用すれば、ソフトウェアの正確性を保証できます。 （私が間違っている場合は私を修正してください。）述語検査で同じ特性が得られますか？質問自体が正しくない場合、私はお詫び申し上げます。私は本当に述語検査が何をしているのか分からない。述語チェックとは何ですか？
述語は、真または偽の結果に等しいロジックステートメントまたは関数です。
手続き型言語と宣言型言語の両方の述語の最も単純な例は、ガード句とアサーションです。
> if (x != null) then ...
> assert x != null
Hoareの事前条件と事後条件は述語の例です。私は、カプセル化されたステートメントの細分性に関して、Hoareに明白なことはないと思っています。単一のステートメント、関数、またはプロセス全体である可能性があります。
不変量は、条件の前の条件である述語の特殊なケースです。
恐らく最も純粋な例はPrologです。ここで、文は述語です。別の例は、Eiffelで使用されているようなdesign-by-contractであり、LISPの空のリストも述語です。
私は、正確性が述語に準拠しているという資格を外して、「ソフトウェアの正確性を保証する」ことに同意することを嫌うだろう。
更新