Для доказательства полной корректности (завершимости) блок-схемы без циклов необходимо выписать следующие два условия завершимости для каждого оператора CALL (с доменом \(D_{res}\), функциями \(f_{arg}\) и \(f_{res}\) и спецификацией \((\varphi_s,~\psi_s)\)) и для каждого пути \(\alpha\) от псевдосвязки START в связку, входящую в этот оператор (на пути имеется ровно \(N\) операторов CALL):
\(\forall \bar{x} \in D_{\bar{x}}~\forall \bar{y} \in D_{\bar{y}} ~\forall r_1 \in D_{res_1}~… \forall r_N \in D_{res_N}~\cdot \\
\varphi(\bar{x})~\land~R_\alpha(\bar{x},~\bar{y}, r_1, …)~\Rightarrow
f_{arg}(\bar{x},~\bar{y}) \neq \omega \land \varphi_s(f_{arg}(\bar{x},~\bar{y}))\)
\(\forall \bar{x} \in D_{\bar{x}}~\forall \bar{y} \in D_{\bar{y}} ~\forall r_1 \in D_{res_1}~…\forall r_N \in D_{res_N} \forall r \in D_{res}\cdot\\
\varphi(\bar{x})~\land~R_\alpha(\bar{x},~\bar{y}, r_1,…)~\land~f_{arg}(\bar{x},~\bar{y}) \neq \omega \land \psi_s(f_{arg}(\bar{x},~\bar{y}), r) ~\Rightarrow~ f_{res}(\bar{x},~\bar{y},~r) \neq \omega\)