検証済み関数型アルゴリズム