変成関係

$f : X \to Y$ を（正しい）関数とする。写像 $g : X \to X$ と $h : Y \to Y$ の組 $(g, h)$ が、すべての $x \in X$ について

を満たすとき、$(g, h)$ を $f$ の変成関係という。$f$ の実装 $\tilde f : X \to Y$ に対する、入力 $x$ での $(g, h)$ の検査とは、$\tilde f(g(x)) = h(\tilde f(x))$ を確かめることをいう。