プログラムの正当性の確率的検証法に関する基礎的研究

点击翻译按钮获取中文摘要

これまでにchecker,self-tester及びself-correctorに関して-(1)関数fがcheckerを持つならば,任意の0<δ【less than or equal】1に対してfは(1,δ)-self-testerを持つ;(2)任意の0【less than or equal】ε_1<ε_2【less than or equal】ε【less than or equal】1に対して,関数fが(ε_1,ε_2)-self-testerとε-self-correctorを持つならば,任意の0<δ【less than or equal】1に対してfは(0,δ)-self-testerを持つ-が知られている.関数fに対して(ε_1,ε_2)-self-testerを設計する際に-(a)要求されるプログラム品質に応じてε_1は任意の設定できること;(b)self-testerの信頼性の意味から|ε_1-ε_2|はできるだけ小さな値をとるいこと-が実用上重要である.従って上記の結果(2)は,δ【similar or equal】0とすることで要求事項(b)は満たすが,本質的に要求事項(a)は満たしていないことが分かる.そこで本研究では,先ず上記の結果(1)に関連して「関数fがcheckerを持つならば,任意の0<ε【less than or equal】1に対してfはε-self-correctorを持つか?」という問題を提起し,以下のような主要結果1:一方向性置換が存在するならば,checkerを持つが,任意の0<ε【less than or equal】1に対してε-self-correctorを持たないような関数f次に要求事項(a)及び(b)を満たすようなself-testerの構成法を確立するために,“self-improver"という新しい概念を提案し,それに基づいて以下のような結果を導出した.主要結果2:任意の0<ε´_1<ε´_2【less than or equal】ε´<1に対して,関数fが(ε´_1,ε´_2)-self-testerとε´-self-correctorを持つならば,ε_1【less than or equal】ε´を満たす任意の0<ε_1<ε_2【less than or equal】1に対して,fは(ε_1,ε_2)-self-testerを持つ,主要結果3:任意の0<ε´_1<ε´_2【less than or equal】ε´<1に対して,関数fが(ε´_1,ε´_2)-self-testerとε´-self-correctorを持つならば,δ【less than or equal】ε´を満たす任意のδ>0に対して,fは(ε´,δ)-self-improverを持つ.