検査・違反・誤りと警告

検査とは、文書の集合 $K$ に、違反の有限集合 $\kappa(K)$ を対応させる手続きである。同じ $K$ に対していつ実行しても同じ集合を返すとき、検査は決定的であるという。違反のうち、1 件でもあればパイプラインを止めるものを誤り、報告するだけで止めないものを警告という。検査が合格であるとは、誤りが 1 件もないことをいう。