|
JAIST Repository >
i. 北陸先端科学技術大学院大学(JAIST) >
i70. JAIST PRESS 発行誌 >
JAIST PRESS 発行資料 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/16096
|
| タイトル: | 法令工学の実践 国民年金法の述語論理による記述と検証 |
| 著者: | 片山, 卓也 |
| 発行日: | Jul-2023 |
| 出版者: | JAIST Press |
| 抄録: | 国民年金法のような行政サービスに関する法令は，その内容は明確であり，文章上の見かけの複雑さの割には論理的深度は深くない．したがって，論理式などの形式的体系によってその内容を記述することにより，可読性が高く，機械的なテストや分析が可能な法令記述が得られる可能性が高い．このような法令は我々の社会の制度的基盤であり，その実働化IT システムが我々の社会生活を支えていることを考えると，法令に対する形式的技術の確立は非常に重要である. 本書は，このような立場から国民年金法の基本的条文の述語論理による記述と定理自動証明器（SMT ソルバー）Z3Py による検証について述べたものである．近年の定理証明技術の進歩や計算機システムの高性能化により，このような技術は行政サービスを規定する法令の作成や管理のための基盤技術になりえるものと考える． また，定理自動証明器は条文論理式の実行機構という側面を持ち，法令実動化IT システムの基本アーキテクチャと考えることができる．度重なる法令改正への対応により現在の法令実働化ITシステムの内部構造の劣化が進み，保守の困難性が社会的な問題となっているが，本書で紹介する法令の形式化・検証技術はこの問題に対する有力な解決法になると期待できる． 本書は2 部から構成されている． 第I 部はこのような新しい法令作成方法論の原理的可能性を示すために書かれた，日本ソフトウェア科学会誌「コンピュータソフトウェア」36 巻3 号(2019) に掲載された論文をそのままの形で転載したものである． 第II 部は，第I 部で述べた内容を事例の面から補強するために，そこで紹介した方法を国民年金法のより多くの条文へ適用した結果を詳細かつ具体的に述べたものであり，このような手法が広く実践される助けとなることを目的としたものである．各条文ごとに，(1) 条文の文章，(2) 論理式記述，(3) 検証スクリプトと検証結果，(4) それらの内容に関するメモを掲載した． 論理式記述は，マクロ表現を用いてなるべく簡潔になるように心懸けたが，これらのマクロの定義などを基本用語定義集として纏めた．これには日付や期間，月数，年齢，イベント成立の前後関係などが含まれ，年金法に内在する時間の構造を表現している． 一方，検証においてはテストデータとしての年金原簿が必要であるが，各条文の検証に必要な複数の年金原簿も纏めて収録した．また，日付けを代数的抽象データとして扱った検証事例や論理式記述に基づく年金システムシミュレーターの構成の概略なども収録した． 最後に，筆者は年金サービスに関する専門家ではなく，本書の論理式化は筆者が注釈書[1, 2] などを頼りに条文を理解することにより行ったものである．この点において専門家から見た場合には条文の理解に不備がある可能性はあるが，最終的な結論である行政サービスに関する法令の論理式化と形式検証の可能性については，大きな間違いはないと考えている．この点も含め，内容に関する疑義に関してはご指摘いただければ幸いである． |
| 記述: | 2019年10月 第1版発行 / 2019年11月 第2版発行 / 2020年11月 第3版発行 / 2021年12月 第4版発行 / 2023年7月 第5版発行 / ISBN:978-4-903092-53-9
2023年7月5日 第5版公開
[第１版からの変更] 第十四条年金原簿：変更，第九十四条保険料の追納：追加
[第2版からの変更] 変更，修正(第十四条 年金原簿，第八条 資格取得の時期，第九条 資格喪失の時期，年金原簿の記述法)，述語名の変更(第二十六条，第二十八条)，追加（第九十四条 保険料の追納，附則（平成一六年六月一一日法律第一〇四号）第十九条)，追加(実際の暦による日付けの記述)，追加(論理式記述に基づく年金システムシミュレーターの構成の概略)
[第３版からの主な変更]・条文論理式において他の条文や年金原簿で定義された述語をインポートし参照する形式を「述語名」から{「条文番号」,「年金原簿名」}.「述語名」に変更した．これにより，条文間の関連が明確となると同時に，年金原簿の操作の前後における変更の記述が明確となった．・検証で必要とする年金原簿，基本用語定義集の設定内容を検証スクリプト内に直接記述する方式に変更した．・基本用語定義集definitions,definitions_date において，事由成立の前後関係オペレータの名称と関数性を変更した．充足リスト，月数定義アルゴリズムの最適化を行った．
[第４版からの主な変更]・用語定義集definitions_date_3 における通日⇔西暦年月日変換において多用される実数除算＋floor 関数の実現が大井によるquot 関数により極めて簡単に実現できることが判明し[4]，これまでの量限定子を用いる方法に代えてこれを採用した． ・期間，月数などの日付オペレータについては，量限定子を用いた論理式による定義に先だって，充足性判定で行うPython 版を優先して使用する形にした． ・条文論理式の表現が条文の文章としても読み下せることを考え，他の条文で定義される述語の参照の方式を，条文番号・述語名の形式から述語名の形式に戻した． ・「論理式記述に基づく年金システムシミュレーターの構成」の内容を改めた． ・第八条，第九条のノートの記述を改めた． |
| 言語: | jpn |
| URI: | http://hdl.handle.net/10119/16096 |
| ISBN: | 978-4-903092-53-9 |
| 出現コレクション: | JAIST PRESS 発行資料 (JAIST PRESS Articles)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| fulltext5-2.pdf | | 714Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
