CBMC (C の境界付きモデル チェッカー) のようなモデル チェッカーでは、ユーザー定義の assert ステートメントはブール条件を取り、モデル チェッカーはプログラムのすべての可能な実行に対して条件が true か false かをチェックします。
C プログラミングでは、ヘッダー ファイル assert.h で assert() マクロを定義します。assert() マクロは、パラメーターが TRUE と評価された場合に TRUE を返し、FALSE と評価された場合に何らかのアクションを実行します。多くのコンパイラは、失敗した assert() でプログラムを中止します。
モデルチェックとプログラミングの世界で、これら2つのアサーションの違いを誰かが明確にすることができますか?
モデルチェックでは、アサート（あなたが言ったように）可能なすべての実行について検証されます（これがモデルチェッカーの主な目的です）。したがって、それが真であれば、何が起こっても条件が常に保持されることがわかります。これは正式な検証の分野です。
C では、アサートは実行時に検証されます。つまり、実行の特定のインスタンスに対して検証されますが、別の実行でそれが true になるという保証はありません。これはテストの分野です。
C の場合、が含まれているNDEBUGときに が定義されているかどうかによって異なります。assert.h
NDEBUGが定義されていない場合は、assert結果が false になり、標準エラーにメッセージが出力され、プログラムが終了します。
NDEBUGが定義されている場合assert、コードは生成されません。つまり、チェックはスキップされます。
http://man7.org/linux/man-pages/man3/assert.3.htmlも参照してください。