規模の大きな，制御フローの複雑なプログラムを充分にテストすることは容易ではない．プログラム実行時の動作の正しさを調べるには，実行時点での性質や条件を示す表明(アサーション) を挿入する方法が知られている． 本論文では，Hoare の記法P{Q}Rに基づいて，事前条件(P)に対して，事前チェック(pre-check ∼P)，および，事後条件(R)に対して，事後チェック(post-check ∼R)するプログラムの設計法を提案する．また，そのようなチェック機能を，能動関数(active function) を用いた形で設計・実現する方法について述べる．能動関数は，自ら起動する条件を持った関数で，指示された時点で条件の値が真(true)になると，関数の本体を実行する． このような設計法によって，実行の正しさを保証するだけでなく，ソフトウェアの仕様の変更に柔軟に対応して，安定した状態を保つプログラムの構成を目指している．なお，能動関数を用いたプログラムを効率良く実行するには，それに適合したハードウェアの支援が不可欠である．