著者

片山 卓也

出版者

JAIST Press

巻号頁・発行日

pp.1-146, 2021-12

---

国民年金法のような行政サービスに関する法令は,その内容は明確であり,文章上の見かけの複雑さの割には論理的深度は深くない.したがって,形式的手法によってその内容を記述することにより,可読性が高く,機械的なテストや分析が可能な法令記述が得られる可能性が高い.また,このような法令は我々の社会の制度的基盤であり,その法令実働化IT システムが我々の社会生活を 支えていることを考えると,法令に対する形式的技術の確立は重要である. 本書は,このような立場から行政サービスに関する法令を意図した通りに正しく作る上で,法令の形式的記述と自動検証技術の可能性を,国民年金法の基本的条文の述語論理による記述と定理自動証明器(SMT ソルバー)Z3Py による検証事例に基づいて述べたものである.近年の定理証明技術の進歩や計算機システムの高性能化により,このような技術は十分に実用化可能であるというのが本書の結論である.法令の度重なる改正に対応するため法令実働化ITシステムの内部構造劣化が進み,保守の困難性が社会的な問題となっているが,本書で述べる技術はこの問題に対する有力な解決法になると思われる. 本書は2部から構成されている. 第I部はこのような新しい法令作成方法論の原理的可能性を示すために書かれた,日本ソフトウェア科学会誌「コンピュータソフトウェア」36巻3号(2019)に掲載された論文をそのままの形で転載したものである. 被保険者の資格,年金の支給期間及び支払期月,併給の調整に関する3 つの典型的条文を通して,論理式化の方法やその構造化の方法等を示すと同時に,検証に必要なテストデータとしての年金原簿の扱いなどについて述べている.また,条文の誤りの定理証明システムによる検証例について述べている. 第II部は,第I部で述べた内容を事例の面から補強するために,そこで紹介した方法を国民年金法のより多くの条文へ適用した結果を詳細かつ具体的に述べたものであり,このような手法を広く実践する際の助けとなることを目的としたものである. 各条文ごとに,(1)条文の文章,(2)論理式記述,(3)検証スクリプトと検証結果,(4)それらの内容に関するメモを付加した.論理式記述は,パターン表現を用いてなるべく簡潔になるように心懸けたが,このようなパターンの定義などを基本用語定義集として纏めた.検証においてはテストデータとしての年金原簿が必要であるが,各条文の検証に必要な複数の年金原簿も纏めて収録した.最後に,日付けを抽象データとして扱った検証事例,実際の暦による日付け記述,論理式記述に基づく年金システムシミュレーターの構成の概略などを収録した.