Mercurial > hg > Papers > 2023 > soto-master
changeset 17:785dd684c529
Fix
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Feb 2023 20:52:51 +0900 |
| parents | 40a9af45b375 |
| children | 1b000d9505f5 |
| files | Paper/master_paper.out Paper/master_paper.pdf Paper/master_paper.tex Paper/reference.bib Paper/tex/abst.tex Paper/tex/abstract.tex Paper/tex/agda.tex Paper/tex/cbc.tex Paper/tex/cbc_agda.tex Paper/tex/conclusion.tex Paper/tex/continuation_agda.tex Paper/tex/dpp_impl.tex Paper/tex/future.tex Paper/tex/hoare.tex Paper/tex/intro.tex Paper/tex/main.tex Paper/tex/rbt_imple.tex Paper/tex/rbt_intro.tex Paper/tex/rbt_verif.tex Paper/tex/spec.tex Paper/tex/spin_dpp.tex Paper/tex/thanks.tex Paper/tex/tree_desc.tex Paper/tex/while_loop.tex |
| diffstat | 24 files changed, 669 insertions(+), 676 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/master_paper.out Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/master_paper.out Thu Feb 02 20:52:51 2023 +0900 @@ -2,9 +2,9 @@ \BOOKMARK [0][]{chapter*.3}{\376\377\170\024\172\166\225\242\220\043\212\326\145\207\151\155\176\076}{}% 1 \BOOKMARK [0][]{chapter.1}{\376\377\173\054\0001\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\327\060\355\060\260\060\351\060\340\060\156\151\034\212\074}{}% 2 \BOOKMARK [0][]{chapter.2}{\376\377\173\054\0002\172\340\000\040\000C\000o\000n\000t\000i\000n\000u\000a\000t\000i\000o\000n\000\040\000b\000a\000s\000e\000d\000\040\000C}{}% 3 -\BOOKMARK [1][]{section.2.1}{\376\377\0002\000.\0001\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\000/\000\040\000D\000a\000t\000a\000\040\000G\000e\000a\000r}{chapter.2}% 4 +\BOOKMARK [1][]{section.2.1}{\376\377\0002\000.\0001\000\040\000C\000o\000d\000e\000G\000e\000a\000r\000\040\000/\000\040\000D\000a\000t\000a\000G\000e\000a\000r}{chapter.2}% 4 \BOOKMARK [1][]{section.2.2}{\376\377\0002\000.\0002\000\040\000C\000b\000C\000\040\060\150\000\040\000C\212\000\212\236\060\156\220\125\060\104}{chapter.2}% 5 -\BOOKMARK [1][]{section.2.3}{\376\377\0002\000.\0003\000\040\000M\000e\000t\000a\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\000/\000\040\000M\000e\000t\000a\000\040\000D\000a\000t\000a\000\040\000G\000e\000a\000r}{chapter.2}% 6 +\BOOKMARK [1][]{section.2.3}{\376\377\0002\000.\0003\000\040\000M\000e\000t\000a\000\040\000C\000o\000d\000e\000G\000e\000a\000r\000\040\000/\000\040\000M\000e\000t\000a\000\040\000D\000a\000t\000a\000G\000e\000a\000r}{chapter.2}% 6 \BOOKMARK [0][]{chapter.3}{\376\377\173\054\0003\172\340\000\040\133\232\164\006\212\074\146\016\145\057\143\364\174\373\212\000\212\236\000\040\000A\000g\000d\000a}{}% 7 \BOOKMARK [1][]{section.3.1}{\376\377\0003\000.\0001\000\040\000A\000g\000d\000a\060\156\127\372\147\054}{chapter.3}% 8 \BOOKMARK [1][]{section.3.2}{\376\377\0003\000.\0002\000\040\000A\000g\000d\000a\060\153\060\210\060\213\133\232\164\006\212\074\146\016}{chapter.3}% 9 @@ -12,14 +12,14 @@ \BOOKMARK [1][]{section.4.1}{\376\377\0004\000.\0001\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000M\000e\000t\000a\000\040\000G\000e\000a\000r\000s}{chapter.4}% 11 \BOOKMARK [0][]{chapter.5}{\376\377\173\054\0005\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\133\232\164\006\212\074\146\016}{}% 12 \BOOKMARK [1][]{section.5.1}{\376\377\0005\000.\0001\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c}{chapter.5}% 13 -\BOOKMARK [2][]{subsection.5.1.1}{\376\377\0005\000.\0001\000.\0001\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\153\060\210\060\213\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\060\156\151\034\212\074\142\113\154\325\000\040}{section.5.1}% 14 -\BOOKMARK [1][]{section.5.2}{\376\377\0005\000.\0002\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\146\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\222\165\050\060\104\060\137\151\034\212\074\060\156\117\213}{chapter.5}% 15 -\BOOKMARK [2][]{subsection.5.2.1}{\376\377\0005\000.\0002\000.\0001\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\133\237\210\305}{section.5.2}% 16 -\BOOKMARK [2][]{subsection.5.2.2}{\376\377\0005\000.\0002\000.\0002\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\151\034\212\074}{section.5.2}% 17 -\BOOKMARK [1][]{section.5.3}{\376\377\0005\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{chapter.5}% 18 -\BOOKMARK [2][]{subsection.5.3.1}{\376\377\0005\000.\0003\000.\0001\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\147\050\151\313\220\040\060\156\212\055\212\010}{section.5.3}% 19 -\BOOKMARK [2][]{subsection.5.3.2}{\376\377\0005\000.\0003\000.\0002\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\133\237\210\305}{section.5.3}% 20 -\BOOKMARK [2][]{subsection.5.3.3}{\376\377\0005\000.\0003\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{section.5.3}% 21 +\BOOKMARK [1][]{section.5.2}{\376\377\0005\000.\0002\000\040\000I\000n\000v\000a\000r\000i\000a\000n\000t\000\040\060\222\165\050\060\104\060\137\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\153\060\210\060\213\151\034\212\074\060\156\145\271\154\325\000\040}{chapter.5}% 14 +\BOOKMARK [1][]{section.5.3}{\376\377\0005\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\146\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\222\165\050\060\104\060\137\151\034\212\074\060\156\117\213}{chapter.5}% 15 +\BOOKMARK [2][]{subsection.5.3.1}{\376\377\0005\000.\0003\000.\0001\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\133\237\210\305}{section.5.3}% 16 +\BOOKMARK [2][]{subsection.5.3.2}{\376\377\0005\000.\0003\000.\0002\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\151\034\212\074}{section.5.3}% 17 +\BOOKMARK [1][]{section.5.4}{\376\377\0005\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{chapter.5}% 18 +\BOOKMARK [2][]{subsection.5.4.1}{\376\377\0005\000.\0004\000.\0001\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\147\050\151\313\220\040\060\156\212\055\212\010}{section.5.4}% 19 +\BOOKMARK [2][]{subsection.5.4.2}{\376\377\0005\000.\0004\000.\0002\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\133\237\210\305}{section.5.4}% 20 +\BOOKMARK [2][]{subsection.5.4.3}{\376\377\0005\000.\0004\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{section.5.4}% 21 \BOOKMARK [0][]{chapter.6}{\376\377\173\054\0006\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{}% 22 \BOOKMARK [1][]{section.6.1}{\376\377\0006\000.\0001\000\040\060\342\060\307\060\353\151\034\147\373\060\150\060\157}{chapter.6}% 23 \BOOKMARK [1][]{section.6.2}{\376\377\0006\000.\0002\000\040\000D\000i\000n\000i\000n\000g\000\040\000P\000h\000i\000l\000o\000s\000o\000p\000h\000e\000r\000s\000\040\000P\000r\000o\000b\000l\000e\000m}{chapter.6}% 24
--- a/Paper/master_paper.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/master_paper.tex Thu Feb 02 20:52:51 2023 +0900 @@ -123,30 +123,9 @@ \input{tex/while_loop.tex} % while loop の実装と検証(簡単に) \input{tex/tree_desc.tex}% Gears Agda における木構造の設計 -\input{tex/spin_dpp.tex}% Gears Agda の記法 loopのやつやる -\input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる - -\chapter{まとめと今後の展望} -本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた.そこで,定理証明については Invariant を用いて定理証明を行った.モデル検査については Gears Agda にて dead lock を検知できるようになった. - -実際に Invariant を用いることで,プログラムに与える入力とその出力に対して条件を与え,Hoare Logic による検証を行えるようになった. -これにより,いままでより容易に Gears Agda にて検証が進められるようになった. - -また,先行研究での課題にて,CbCで開発,検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列動作の検証があった.これもモデル検査により,Gears Agda 内で並列動作に対する検証も行えるようになった. - - -\section{今後の課題} -今後の課題としてモデル検査による検証,定理証明による検証,Gears Agda の今後の展望について述べる. -モデル検査においては,有向グラフからなる有限オートマトンの遷移を全自動探索することと,live lockやLTTLも用いたアサーションなどの検証\cite{model}を行いたい. -加えて,State List のデータ構造を balanced tree にすることで,並列にモデル検査が行えるようになると考えられる. -これにより,状態が膨大になるモデル検査に対応できる. - -定理証明においては,Red Black Tree の検証を行いたいと思っている. -これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている. - -Gears Agda の展望について,CbC に変換することが挙げられる. -CbC はアセンブラに近いため記述が複雑かつ困難であるが,Gears Agda で記述したものを CbC に変換できるようになれば,その点を解決できる.更に,Gears Agda で検証を行ったプログラムであるため,プログラムの信頼性もある. -加えて,モデル検査の実行には速度が求められるが,CbCで高速に実行できるようになることが期待される. +\input{tex/spin_dpp.tex} +\input{tex/dpp_impl.tex} +\input{tex/conclusion.tex} % %謝辞 \input{tex/thanks.tex}
--- a/Paper/reference.bib Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/reference.bib Thu Feb 02 20:52:51 2023 +0900 @@ -100,7 +100,7 @@ @inproceedings{mitsuki-prosym, author = "宮城光希 and 河野真治", - title = "Code Gear と Data Gear を持つ Gears OS の設計", + title = "CodeGear と DataGear を持つ Gears OS の設計", booktitle = "第59回プログラミング・シンポジウム予稿集", year = "2018", volume = "2018",
--- a/Paper/tex/abst.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/abst.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,30 +1,30 @@ \chapter*{要旨} -開発手法の一つとして，形式手法というものがある． -形式手法とはプログラムの仕様を形式化，つまり数学的な記述を行い， -書いたプログラムがそれを満たしているか検証を行う開発手法である． -代表的な形式の検証手法として，定理証明やモデル検査が挙げられる． +開発手法の一つとして、形式手法というものがある。 +形式手法とはプログラムの仕様を形式化、つまり数学的な記述を行い、 +書いたプログラムがそれを満たしているか検証を行う開発手法である。 +代表的な形式の検証手法として、定理証明やモデル検査が挙げられる。 -形式手法で開発したプログラムは数学的に正しいことが証明されている. -そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている． -一見完璧な手法であるように思えるが欠点として，形式化や検証が複雑なため膨大なコストを要する． -シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用する利点が薄くなる． +形式手法で開発したプログラムは数学的に正しいことが証明されている。 +そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている。 +一見完璧な手法であるように思えるが欠点として、形式化や検証が複雑なため膨大なコストを要する。 +シンプルな実装であれば仕様の形式化が容易に行えるが、そうであれば形式手法を使用する利点が薄くなる。 -そのため，他のプログラミング言語と比べて検証に適している Gears Agda を使用する． +そのため、他のプログラミング言語と比べて検証に適している Gears Agda を使用する。 Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を -取り入れた記法で記述された定理証明支援器 Agda のことである． +取り入れた記法で記述された定理証明支援器 Agda のことである。 -定理証明によるプログラムの検証は一般的に難易度が高いが， -Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている． +定理証明によるプログラムの検証は一般的に難易度が高いが、 +Gears Agda では検証をプログラム単位に分割することができ、比較的容易に検証を行えるようになっている。 -先行研究では implies を用いて Hoare Logic での定理証明を行っていた. -しかし、それでは記述が長く複雑になっていた. -そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行をすることで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった. +先行研究では implies を用いて Hoare Logic での定理証明を行っていた。 +しかし、それでは記述が長く複雑になっていた。 +そこで今回は Invariant というプログラムの不変条件を新たに取り入れた。これを検証しながら実行をすることで、Hoare Logic を用いた定理証明を比較的簡単に行えるようになった。 -また，定理証明では並列処理の検証は困難である。出現する状態を一度全て出してからそれらの検証を行わないといけないためである。 -そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした． +また、定理証明では並列処理の検証は困難である。出現する状態を一度全て出してからそれらの検証を行わないといけないためである。 +そのため、もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした。 -これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる。 +これらのことから、本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる。 \chapter*{Abstract} One of the development methods is called formal methods.
--- a/Paper/tex/abstract.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/abstract.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,8 +1,8 @@ \renewcommand{\abstractname}{\normalsize 要 旨} \begin{abstract} - 当研究室にて Continuation based C\cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している． - 先行研究\cite{ryokka-master}にて Floyd-Hoare Logic\cite{hoare}(以下Hoare Logic)を用いてその検証を行なった． - 本稿では，先行研究にて実施されなかった CbC における RedBlackTree の検証を Hoare Logic を用いて検証することを目指す． + 当研究室にて Continuation based C\cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している。 + 先行研究\cite{ryokka-master}にて Floyd-Hoare Logic\cite{hoare}(以下Hoare Logic)を用いてその検証を行なった。 + 本稿では、先行研究にて実施されなかった CbC における RedBlackTree の検証を Hoare Logic を用いて検証することを目指す。 \end{abstract} \renewcommand{\abstractname}{\normalsize Abstract}
--- a/Paper/tex/agda.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/agda.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,106 +1,106 @@ \chapter{定理証明支援系言語 Agda} -Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である． -Agda は依存型という型システムを持ち，型を第一級オブジェクトとして扱う． +Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である。 +Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。 -また,もともとの Agda には自然数などの普遍的な定義すら存在しない. -その実装ができることも本章で取り扱っているが,一般的には agda-standard-libralies \cite{agda-stdlib} を使用する. +また、ともとの Agda には自然数などの普遍的な定義すら存在しない。 +その実装ができることも本章で取り扱っているが、般的には agda-standard-libralies \cite{agda-stdlib} を使用する。 -本章ではAgdaの基本とAgdaによる定理証明の方法について述べる. +本章ではAgdaの基本とAgdaによる定理証明の方法について述べる。 \section{Agdaの基本} -Agda の記述ではインデントが意味を持ち，スペースの有無もチェックされる． -コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される． -また，\verb/_/でそこに入りうるすべての値を示すことができ， -\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる． +Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。 +コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 +また、\verb/_/でそこに入りうるすべての値を示すことができ、 +\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 %% データについて -Agda では型をデータや関数に記述する必要がある． -Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する． -このとき \verb/name/ に 空白があってはいけない． -データ型は，代数的なデータ構造で，その定義には \verb/data/ キーワードを用いる． -\verb/data/ キーワードの後に \verb/data/ の名前と，型， \verb/where/ 句を書きインデントを深くし， -値にコンストラクタとその型を列挙する． +Agda では型をデータや関数に記述する必要がある。 +Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。 +このとき \verb/name/ に 空白があってはいけない。 +データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 +\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、 +値にコンストラクタとその型を列挙する。 -\coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)の例である． +\coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)の例である。 \lstinputlisting[label=code:agda-nat, caption=自然数を表すデータ型 $\mathbb{N}$ の定義] {src/nat.agda.replaced} -\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である． -\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を返す再帰的なデータになっており， -\verb/suc/ を連ねることで自然数全体を表現することができる． +\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。 +\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を返す再帰的なデータになっており、 +\verb/suc/ を連ねることで自然数全体を表現することができる。 -$\mathbb{N}$ 自身の型は \verb/Set/ であり，これは Agda が組み込みで持つ「型集合の型」である． -\verb/Set/ は階層構造を持ち，型集合の集合の型を指定するには \verb/Set1/ と書く． -%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる． +$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 +\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。 +%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。 Agda には C 言語における構造体に相当するレコード型というデータも存在する。 -例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する．\coderef{agda-record}のようになる． +例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{agda-record}のようになる。 \lstinputlisting[label=code:agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced} -レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する． -複数の値を列挙するには \verb/;/ で区切る必要がある． +レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 +複数の値を列挙するには \verb/;/ で区切る必要がある。 %% 関数について -Agda での関数は型の定義と，関数の定義をする必要がある． -関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが，入力を受け取り出力を返す型として記述される．または $\rightarrow$ を用いて \verb/input → output/ のように記述される． -また，\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し，中間記法で関数を定義することもできる． -関数の定義は型の定義より下の行に，\verb/=/ を使い \verb/name input = output/ のように記述される． +Agda での関数は型の定義と、関数の定義をする必要がある。 +関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力を返す型として記述される。または $\rightarrow$ を用いて \verb/input → output/ のように記述される。 +また、\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。 +関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。 -例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる． -また，複数の引数を取る関数の型は \verb/A → A → B/ のように書ける． -例として任意の自然数$\mathbb{N}$を受け取り，\verb/+1/した値を返す関数はCode \ref{agda-function}のように定義できる． -\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} +例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。 +また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。 +例として任意の自然数$\mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{agda-function}のように定義できる。 +\lstinputlisting[label=code:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} -引数は変数名で受けることもでき，具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる． -これはパターンマッチと呼ばれ，コンストラクタで case 文を行なっているようなものである． -例として自然数$\mathbb{N}$の加算を関数で書くとCode \ref{agda-plus}のようになる． +引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 +これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 +例として自然数$\mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。 -\lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} +\lstinputlisting[label=code:agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} %% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} -パターンマッチでは全てのコンストラクタのパターンを含む必要がある． -例えば，自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある． -なお，コンストラクタをいくつか指定した後に変数で受けることもでき，その変数では指定されたもの以外を受けることができる． -例えばCode \ref{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る． +パターンマッチでは全てのコンストラクタのパターンを含む必要がある。 +例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。 +なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。 +例えば\coderef{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。 -\lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} +\lstinputlisting[label=code:agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} -Agda には$\lambda$計算が存在している．$\lambda$計算とは関数内で生成できる無名の関数であり， -\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる． -Code \ref{agda-function} で例とした \verb/+1/ をラムダ計算で書くとCode \ref{agda-lambda}の\verb/$\lambda$+1/ように書くことができる．この二つの関数は同一の動作をする． +Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、 +\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。 +\coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。 -\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} +\lstinputlisting[label=code:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} -Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる． -スコープは \verb/where/句が存在する関数内部のみであるため，名前空間が汚染させることも無い． -例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき， \verb/where/ を使うとリストCode \ref{agda-where} のように書ける． -これは \verb/f'/ と同様の動作をする． -\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し，改行の後インデントをして関数内部で利用する関数を定義する． +Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 +スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 +例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト\coderef{agda-where} のように書ける。 +これは \verb/f'/ と同様の動作をする。 +\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 -\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} +\lstinputlisting[label=code:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} -また Agda では停止性の検出機能が存在し，プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る． -\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない． -Code \ref{term} で書かれた，\verb/loop/ と \verb/stop/ は任意の自然数を受け取り，0になるまでループして0を返す関数である． -\verb/loop/ では $\mathbb{N}$ の数を受け取り， \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる．しかし，\verb/loop/の記述では関数が停止すると言えないため，定義するには\verb/{-# TERMINATING #-}/のタグが必要である． -\verb/stop/ では自然数がパターンマッチで分けられ，\verb/zero/のときは \verb/zero/を返し， \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する． +また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。 +\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。 +\coderef{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。 +\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。 +\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。 -\lstinputlisting[label=term, caption=停止しない関数 loop，停止する関数 stop] {src/termination.agda.replaced} +\lstinputlisting[label=code:term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced} -このように再帰的な定義の関数が停止するときは，何らかの値が減少する必要がある． +このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。 \section{Agdaによる定理証明} -Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式， $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である． -証明の例として \coderef{proof} を見る． -ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している． -これは，引数として受けている \verb/y/ が \verb/Nat/ なので， \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある． +Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 +証明の例として \coderef{proof} を見る。 +ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している。 +これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 \lstinputlisting[caption=等式変形の例,label=code:proof]{src/zero.agda.replaced} -\verb/y = zero/ の時は $zero \equiv zero$ とできて，左右の項が等しいということを表す \verb/refl/ で証明することができる． +\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 \verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという -\coderef{cong}の \verb/cong/ を使って，y の値を 1 減らしたのち，再帰的に \verb/+zero y/ -を用いて証明している． +\coderef{cong}の \verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/ +を用いて証明している。 \lstinputlisting[caption=congの定義,label=code:cong]{src/cong.agda.replaced} %% \begin{lstlisting}[caption=等式変形の例,label=proof] @@ -112,16 +112,16 @@ %% -- cong f refl = refl %% \end{lstlisting} -また，他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している． -ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに，等式を変形する構文の例として加算の交換則について示す． +また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。 +ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。 -\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し，複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する． -\coderef{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である． -ここでは，\verb/+zero/ を利用し， \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり，左右の項が等しいことを示す \verb/refl/ になっている． +\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。 +\coderef{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。 +ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。 \lstinputlisting[caption=congを用いた等式変形の例,label=code:agda-term-post]{src/agda-term3.agda.replaced} -\coderef{agda-term-post} では \verb/suc (y + x)/ $\equiv$ \verb/y + (suc x)/ という等式に対して $\equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $\equiv$ \verb/suc (y + x)/の形にし，\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した． -これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた． +\coderef{agda-term-post} では \verb/suc (y + x)/ $\equiv$ \verb/y + (suc x)/ という等式に対して $\equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $\equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。 +これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。 -Agda ではこのような形で等式を変形しながら証明を行う事ができる． +Agda ではこのような形で等式を変形しながら証明を行う事ができる。
--- a/Paper/tex/cbc.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/cbc.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,73 +1,73 @@ \chapter{Continuation based C} Continuation based C\cite{kaito-lola}は -関数呼び出しの際にjmp命令で遷移をし，環境を持たずに遷移する +関数呼び出しの際にjmp命令で遷移をし、環境を持たずに遷移する ことができるC言語である。 -すなわちC言語の下位言語にあたり，よりアセンブラに近い記述を行う． +すなわちC言語の下位言語にあたり、よりアセンブラに近い記述を行う。 -CbC では CodeGear を処理の単位， -DataGear をデータの単位として記述するプログラミング言語である． +CbC では CodeGear を処理の単位、 +DataGear をデータの単位として記述するプログラミング言語である。 -jmp命令で関数遷移するため関数遷移し実行が終了しても，もとの関数に戻ることはない． -そのため次に遷移する Code Gear を指定する． -したがって，Code Gear に Deta Gear を与え，それをもとに処理を行い， -出力として Data Gear を返し，また次の Code Gearに遷移していく流れとなる． +jmp命令で関数遷移するため関数遷移し実行が終了しても、もとの関数に戻ることはない。 +そのため次に遷移する CodeGear を指定する。 +したがって、CodeGear に Deta Gear を与え、それをもとに処理を行い、 +出力として DataGear を返し、また次の CodeGearに遷移していく流れとなる。 -本章ではCbCの概要について説明する. +本章ではCbCの概要について説明する。 -\section{Code Gear / Data Gear} -CbCでは,検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる. +\section{CodeGear / DataGear} +CbCでは,検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。 -CodeGear はプログラムの処理そのものであり,一般的なプログラム言語における関数と同じ役割である. -DataGear は CodeGear で扱うデータの単位であり,処理に必要なデータである. -CodeGear の入力となる DataGear を Input DataGear と呼び,出力は Output DataGear と呼ぶ. +CodeGear はプログラムの処理そのものであり,一般的なプログラム言語における関数と同じ役割である。 +DataGear は CodeGear で扱うデータの単位であり,処理に必要なデータである。 +CodeGear の入力となる DataGear を Input DataGear と呼び,出力は Output DataGear と呼ぶ。 -CodeGear 間の移動は継続を用いて行われる. -継続は関数呼び出しとは異なり,呼び出した後に元のコードに戻れず,次の CodeGear へ遷移を行う. -これは,関数型プログラミングでは末尾再帰をしていることと同義である. +CodeGear 間の移動は継続を用いて行われる。 +継続は関数呼び出しとは異なり,呼び出した後に元のコードに戻れず,次の CodeGear へ遷移を行う。 +これは,関数型プログラミングでは末尾再帰をしていることと同義である。 \section{CbC と C言語の違い} -同じ仕様でCbCとC言語で実装した際の違いを,実際のコードを元に比較する. +同じ仕様でCbCとC言語で実装した際の違いを,実際のコードを元に比較する。 比較するにあたり,再起処理が含まれるコードの例として, -フィボナッチ数列の n 番目を求めるコードを挙げる. -C言語で記述したものが\coderef{fib_c}になり、CbCで記述したものが\coderef{fib_cbc}になる. -CbCは実行を継続するため, return を行えない.そのためC言語での実装も return を書 -かず関数呼び出しを行い,最後にexitをして実行終了するように記述している. +フィボナッチ数列の n 番目を求めるコードを挙げる。 +C言語で記述したものが\coderef{fib_c}になり、CbCで記述したものが\coderef{fib_cbc}になる。 +CbCは実行を継続するため、return を行えない。そのためC言語での実装も return を書 +かず関数呼び出しを行い,最後にexitをして実行終了するように記述している。 \lstinputlisting[label=code:fib_c, caption=C言語で記述した フィボナッチ数列の n 番目 を求めるコード, firstline=5] {src/cbc/fib.c} \lstinputlisting[label=code:fib_cbc, caption=CbCで記述した フィボナッチ数列の n 番目 を求めるコード, firstline=5] {src/cbc/fib.cbc} -軽量実装になっているのか,上記のコードをアセンブラ変換した結果を見て確認する. -全てを記載すると長くなるので,アセンブラ変換した際のfib関数のみを記載する. -C言語で記述したコードをアセンブラ変換した結果が\coderef{c-ass}. -CbCで記述したコードをアセンブラ変換した結果が\coderef{cbc-ass}になる. +軽量実装になっているのか,上記のコードをアセンブラ変換した結果を見て確認する。 +全てを記載すると長くなるので,アセンブラ変換した際のfib関数のみを記載する。 +C言語で記述したコードをアセンブラ変換した結果が\coderef{c-ass}。 +CbCで記述したコードをアセンブラ変換した結果が\coderef{cbc-ass}になる。 比較すると,fib 関数の内部で再度 fib 関数を呼び出す際, -C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している. -対して CbC で実装した\coderef{cbc-ass}の32行目では, jmp により fib 関数に移動 -している. +C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している。 +対して CbC で実装した\coderef{cbc-ass}の32行目では、jmp により fib 関数に移動 +している。 \lstinputlisting[label=code:c-ass, caption=cで記述した際の fib 関数のアセンブラ] {src/cbc/c.txt} \lstinputlisting[label=code:cbc-ass, caption=cbcで記述した際の fib 関数のアセンブラ] {src/cbc/cbc.txt} -以上のことから CbCが軽量継続を行っていると言える. +以上のことから CbCが軽量継続を行っていると言える。 -\section{Meta Code Gear / Meta Data Gear} -Meta DataGear は CbC 上のメタ計算で扱われる DataGear である.例えば stub +\section{Meta CodeGear / Meta DataGear} +Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub CodeGear では Context と呼ばれる接続可能な CodeGear,DataGear のリストや,DataGear -のメモリ空間等を持った Meta DataGear を扱っている. +のメモリ空間等を持った Meta DataGear を扱っている。 -また，プログラムを記述する際は，ノーマルレベルの計算の他に，メモリ管理，スレッド管理，資源管理等を記述しなければならない処理が存在する． -これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ． +また、プログラムを記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。 +これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。 -メタ計算は OS の機能を通して処理することが多く，信頼性の高い記述が求められる． -そのため， CbC ではメタ計算を分離するために Meta CodeGear， Meta DataGear を定義している． +メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。 +そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。 -Meta CodeGear は CbC 上でのメタ計算で，通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である． -図 \ref{fig:meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している． +Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 +\figref{meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している。 \begin{figure}[htpb] \begin{center}
--- a/Paper/tex/cbc_agda.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/cbc_agda.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,73 +1,73 @@ \chapter{GearsAgda 形式で書く Agda} -CbC の継続の概念を取り入れた Agda の記法を説明する． -Agdaでは関数の再帰呼び出しが可能であるが，CbCでは値が帰って来ない．そのためAgda -で実装を行う際には再帰呼び出しを行わないようにする． +CbC の継続の概念を取り入れた Agda の記法を説明する。 +Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が帰って来ない。そのためAgda +で実装を行う際には再帰呼び出しを行わないようにする。 -以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する． +以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する。 -\lstinputlisting[caption= Agdaでの Data Gear の定義, label=agda-dg, firstline=6, lastline=11]{src/agda/cbc-agda.agda.replaced} +\lstinputlisting[caption= Agdaでの DataGear の定義, label=code:agda-dg, firstline=6, lastline=11]{src/agda/cbc-agda.agda.replaced} -\lstinputlisting[caption= Agdaでの Code Gear の定義, label=agda-cg, firstline=12, lastline=16]{src/agda/cbc-agda.agda.replaced} +\lstinputlisting[caption= Agdaでの CodeGear の定義, label=code:agda-cg, firstline=12, lastline=16]{src/agda/cbc-agda.agda.replaced} -Code \ref{agda-dg}が Data Gear の定義をしている． -今回は足し算を実装するので，varx に vary を足すことを考える． -そのためそれらが2つの自然数を持つようにしている． +\coderef{agda-dg}が DataGear の定義をしている。 +今回は足し算を実装するので、varx に vary を足すことを考える。 +そのためそれらが2つの自然数を持つようにしている。 -Code \ref{agda-cg}では Code Gear の定義になる． -最初に Data Gear となる env を受け取ったあと，そのまま次の関数に遷移させている． +\coderef{agda-cg}では CodeGear の定義になる。 +最初に DataGear となる env を受け取ったあと、そのまま次の関数に遷移させている。 -Agda の記述は Curry-Howard 対応になっていて， -最初に関数名のあとに:（コロン）の後ろに命題を記述し， -そのあとに関数名のあとに引数を書き，=（イコール）の後ろに定義を記述している． +Agda の記述は Curry-Howard 対応になっていて、 +最初に関数名のあとに:（コロン）の後ろに命題を記述し、 +そのあとに関数名のあとに引数を書き、=（イコール）の後ろに定義を記述している。 -Gears Agda での Code Gear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で終了するようになっている． -この （Env $\rightarrow$ t） は引数で受け取る型で Env を受け取ってtを返すという意味になる． -これが Code Gear を実行したあとの末尾関数呼び出しを行う次の Code Gear となる． -最後にtを返すのは，これ自体が Code Gear であることを示している． +Gears Agda での CodeGear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で終了するようになっている。 +この （Env $\rightarrow$ t） は引数で受け取る型で Env を受け取ってtを返すという意味になる。 +これが CodeGear を実行したあとの末尾関数呼び出しを行う次の CodeGear となる。 +最後にtを返すのは、これ自体が CodeGear であることを示している。 -引数を受け取ったあとに別の関数に再度渡している． -これは，Agda の繰り返し処理を行う際に停止性を見失うために減少列を引数に取っている． -内部の処理は reducer を減らしながらvarxを増やし， -vary の値を varx に与えていくことで足し算を定義している． -基本的に繰り返し実行するコードを実装する場合には， -実行時に減少しその関数がいずれ停止することを示す reducer を含めるようにしている． +引数を受け取ったあとに別の関数に再度渡している。 +これは、Agda の繰り返し処理を行う際に停止性を見失うために減少列を引数に取っている。 +内部の処理は reducer を減らしながらvarxを増やし、 +vary の値を varx に与えていくことで足し算を定義している。 +基本的に繰り返し実行するコードを実装する場合には、 +実行時に減少しその関数がいずれ停止することを示す reducer を含めるようにしている。 -対照的に reducer を含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す． +対照的に reducer を含めなかった際の CodeGear を \coderef{agda-not-cg}に示す。 -\lstinputlisting[caption= Agdaでの 停止性が示せない CodeGear の例, label=agda-not-cg, firstline=18, lastline=22]{src/agda/cbc-agda.agda.replaced} +\lstinputlisting[caption= Agdaでの 停止性が示せない CodeGear の例, label=code:agda-not-cg, firstline=18, lastline=22]{src/agda/cbc-agda.agda.replaced} -Agdaではパターンマッチを行うことで場合分けを考えることができるが， -受け取った Code Gear であるenvを with を使用してパターンマッチを試みている． -パターンマッチ自体は可能だが，この方法だとAgdaが関数が停止することを認識できない． -そのため，\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし、 -この関数が停止することを記述してコンパイルが通るようにしている． +Agdaではパターンマッチを行うことで場合分けを考えることができるが、 +受け取った CodeGear であるenvを with を使用してパターンマッチを試みている。 +パターンマッチ自体は可能だが、この方法だとAgdaが関数が停止することを認識できない。 +そのため、\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし、 +この関数が停止することを記述してコンパイルが通るようにしている。 -Code \ref{agda-exec-cg} は受け取った引数で Data Gear を初期化して -それを Code Gear に与えることで実行を行っている． +\coderef{agda-exec-cg} は受け取った引数で DataGear を初期化して +それを CodeGear に与えることで実行を行っている。 -\lstinputlisting[caption= Agdaでの CodeGear の初期化, label=agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced} +\lstinputlisting[caption= Agdaでの CodeGear の初期化, label=code:agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced} -今回の例では 引数から Data Gear を作成するのは複雑ではない。 -そのため，一度で Data Gear を作成してそのまま Code Gear に渡している。 -引数から Data Gear を作成するのが複雑な場合は、一度入力から -Data Gear を作成する Code Gear を用いる． -加えて，実行なので命題の部分にある出力の型は Env になっている． +今回の例では 引数から DataGear を作成するのは複雑ではない。 +そのため、一度で DataGear を作成してそのまま CodeGear に渡している。 +引数から DataGear を作成するのが複雑な場合は、一度入力から +DataGear を作成する CodeGear を用いる。 +加えて、実行なので命題の部分にある出力の型は Env になっている。 \section{Agda による Meta Gears} -通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である． +通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 今回は定理証明やモデル検査を行う際に使用する \cite{atton-master}。 \begin{itemize} \item Meta DataGear \mbox{}\\ - Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる． - 通常の Data Gear を wraping している． - 今回はこれを用いることで，定理証明では不変状態の条件を保存し，モデル検査ではその時点での状態を保存する。 + Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 + 通常の DataGear を wraping している。 + 今回はこれを用いることで、定理証明では不変状態の条件を保存し、モデル検査ではその時点での状態を保存する。 \item Meta CodeGear\mbox{}\\ Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear - である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 - す CodeGear である．今回はここで定理証明やモデル検査を行う。 + である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 + す CodeGear である。今回はここで定理証明やモデル検査を行う。 \end{itemize}
--- a/Paper/tex/conclusion.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/conclusion.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,10 +1,22 @@ -\section{まとめ} -本稿では,Gears Agda を用いてAI研究への適応方法について述べた. -手法として,Gears Agda によりプログラムの内部にアルゴリズムを使用したコードで -置き換えられる部分が存在するかをモデル検査で探索する. -これをニューラルネットワークの中間層の最適化に使用する. -したがって,中間層を別の少ないレイヤーで置き換えられないかを探索する. -加えて,考慮するレイヤーの中に新規で計算式を加えることで新しいレイヤーを -開発できるのではないかとも考えている. +\chapter{まとめと今後の展望} +本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで,定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。 + +実際に Invariant を用いることで,プログラムに与える入力とその出力に対して条件を与え,Hoare Logic による検証を行えるようになった。 +これにより,いままでより容易に Gears Agda にて検証が進められるようになった。 + +また,先行研究での課題にて,CbCで開発,検証を行いたいと考えている Gears OS\cite{mitsuki-prosym}の並列動作の検証があった。これもモデル検査により,Gears Agda 内で並列動作に対する検証も行えるようになった。 +\section{今後の課題} +今後の課題としてモデル検査による検証,定理証明による検証,Gears Agda の今後の展望について述べる。 +モデル検査においては,有向グラフからなる有限オートマトンの遷移を全自動探索することと,live lockやLTTLも用いたアサーションなどの検証\cite{model}を行いたい。 +加えて,State List のデータ構造を balanced tree にすることで,並列にモデル検査が行えるようになると考えられる。 +これにより,状態が膨大になるモデル検査に対応できる。 + +定理証明においては,Red Black Tree の検証を行いたいと思っている。 +これで検証を行ったものをモデル検査や Gears OS のファイルシステムなどに転用できると考えている。 + +Gears Agda の展望について,CbC に変換することが挙げられる。 +CbC はアセンブラに近いため記述が複雑かつ困難であるが,Gears Agda で記述したものを CbC に変換できるようになれば,その点を解決できる。更に,Gears Agda で検証を行ったプログラムであるため,プログラムの信頼性もある。 +加えて,モデル検査の実行には速度が求められるが,CbCで高速に実行できるようになることが期待される。 +
--- a/Paper/tex/continuation_agda.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/continuation_agda.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,9 +1,9 @@ -\section{Code Gearに合わせた Agda} -検証を行うために，AgdaのコードもCbCに合わせて記述を行う必要がある． -実際に以下がコードとなる． +\section{CodeGearに合わせた Agda} +検証を行うために、AgdaのコードもCbCに合わせて記述を行う必要がある。 +実際に以下がコードとなる。 -CbCの特徴である，変数を継続して実行するために，必要な変数は Envc に格納する． -コードに (next : Envc → t) と (exit : Envc → t) を引数に受け取っている． -これで次の遷移先を引数として受け取る事で，実行を継続していることを示す． +CbCの特徴である、変数を継続して実行するために、必要な変数は Envc に格納する。 +コードに (next : Envc → t) と (exit : Envc → t) を引数に受け取っている。 +これで次の遷移先を引数として受け取る事で、実行を継続していることを示す。 = の後は next Envc もしくは exit Envc となっていることからも -実行を継続している事が分かる． +実行を継続している事が分かる。
--- a/Paper/tex/dpp_impl.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/dpp_impl.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,203 +1,203 @@ \section{Gears Agdaによるモデル検査の流れ} -今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている. +今回作成した Gears Agda による DPP のモデル検査の流れは以下のようになっている。 \begin{enumerate} \item Gears Agda にて DPP の実装を行う \item プログラムが実行中に取りうる状態の網羅をする State List を作成する - \item 上で実装したものを使用しつつ Meta Data Gear を構築する Meta Code Gearを記述する - \item 上記 Meta Code Gear で作成された meta data を元に,dead lockを判定する Meta Code Gear を記述する - \item 状態を網羅した State List にある State を一つずつ Meta Code Gear に実行させて,dead lockしている状態がないか確認する + \item 上で実装したものを使用しつつ Meta DataGear を構築する Meta CodeGearを記述する + \item 上記 Meta CodeGear で作成された meta data を元に,dead lockを判定する Meta CodeGear を記述する + \item 状態を網羅した State List にある State を一つずつ Meta CodeGear に実行させて,dead lockしている状態がないか確認する \end{enumerate} -先行研究では網羅した状態データを State DB に格納していた.しかし今回の Gears Agda では State List にて代替とした.これは List で行った方が Agda での実装がしやすい点にある.本来は branced tree をデータ構造に持って State を作成するほう正しい. +先行研究では網羅した状態データを State DB に格納していた。しかし今回の Gears Agda では State List にて代替とした。これは List で行った方が Agda での実装がしやすい点にある。本来は branced tree をデータ構造に持って State を作成するほう正しい。 -dead lock の定義として,全てのプロセスが他のプロセスの実行終了待ちをしている.かつ新たに状態の分岐が作成できないものとした. -そこでstep実行してもプロセスがすべて変動がなく,かつStateの分岐が作成されなかったものを dead lock としている. +dead lock の定義として,全てのプロセスが他のプロセスの実行終了待ちをしている。かつ新たに状態の分岐が作成できないものとした。 +そこでstep実行してもプロセスがすべて変動がなく,かつStateの分岐が作成されなかったものを dead lock としている。 -最後について,今回は状態の網羅を一度終了してから dead lock の有無を検証している.しかし,これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである.検証したいプログラムが無限の状態を作成する場合は,Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる.モデル検査中に意図しない動きがあった場合に停止するようにすることで,無限の状態を作成するプログラムであっても,モデル検査ができると考える.他にも,プログラムが取る状態を制限することで有限な状態を作成するようにし,モデル検査をすることもできる. (bounded model checking) +最後について,今回は状態の網羅を一度終了してから dead lock の有無を検証している。しかし,これは今回のプログラムが有限オートマトンであることは事前に明らかであるためにできたことである。検証したいプログラムが無限の状態を作成する場合は,Stateを作成するたびにそれに対して dead lock や live lock などのモデル検査をすることもできる。モデル検査中に意図しない動きがあった場合に停止するようにすることで,無限の状態を作成するプログラムであっても,モデル検査ができると考える。他にも,プログラムが取る状態を制限することで有限な状態を作成するようにし,モデル検査をすることもできる。 (bounded model checking) \section{Gears Agda によるDPPの実装} -DPP の記述の主要部分を示し，説明する． +DPP の記述の主要部分を示し、説明する。 -\lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced} +\lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=code:agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced} -\lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced} +\lstinputlisting[caption= Gears Agdaでの DPP の プロセス , label=code:agda-dpp-process, firstline=9, lastline=16]{src/agda-dpp-impl.agda.replaced} -\lstinputlisting[caption= Gears Agdaでの DPP の Data Gear , label=agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced} +\lstinputlisting[caption= Gears Agdaでの DPP の DataGear , label=code:agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced} -Code \ref{agda-dpp-state}は -前述した哲学者の状態を書き記して，哲学者が今行おうとしている動作を網羅している． +\coderef{agda-dpp-state}は +前述した哲学者の状態を書き記して、哲学者が今行おうとしている動作を網羅している。 -Code \ref{agda-dpp-process}は -哲学者一人ずつの環境を持っている． -pid はその哲学者がどこに座っているかの識別子で， -right / left hand はフォークを手に持っているかを格納している． -next-code は次に行う動作を格納している． +\coderef{agda-dpp-process}は +哲学者一人ずつの環境を持っている。 +pid はその哲学者がどこに座っているかの識別子で、 +right / left hand はフォークを手に持っているかを格納している。 +next-code は次に行う動作を格納している。 -Code \ref{agda-dpp-dg} が Data Gear になる． -phは前もって定義した一人の哲学者のプロセスの List になる． -List になっている理由は，哲学者が複数人いるためである． -そのため実行時にListから一人ずつ取り出して実行をしていく． +\coderef{agda-dpp-dg} が DataGear になる。 +phは前もって定義した一人の哲学者のプロセスの List になる。 +List になっている理由は、哲学者が複数人いるためである。 +そのため実行時にListから一人ずつ取り出して実行をしていく。 -tableはテーブルに置いてあるフォークの状態のことで， -pid が1の人の右側にあるフォークが List の最初にあり， -pid が1の人の左側にあるフォーク，すなわち pid が2の人の右側にあるフォークが -その次の List に格納されていくようになっている． -また，自然数の List になっているが， -その場所のフォークがテーブルの上にある場合は自然数の0が， -誰かが所持している場合はその人の pid が格納されるようになっている． +tableはテーブルに置いてあるフォークの状態のことで、 +pid が1の人の右側にあるフォークが List の最初にあり、 +pid が1の人の左側にあるフォーク、すなわち pid が2の人の右側にあるフォークが +その次の List に格納されていくようになっている。 +また、自然数の List になっているが、 +その場所のフォークがテーブルの上にある場合は自然数の0が、 +誰かが所持している場合はその人の pid が格納されるようになっている。 -\lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced} +\lstinputlisting[caption= Gears Agdaでの DPP の DataGear のinit, label=code:agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced} -Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる． -ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つずつ作成し env を作成している． -また，最初の哲学者の状態は思考することであるため，next-code には C\_thinking を格納している． +\coderef{agda-dpp-init}が入力から DataGear を作成する CodeGear になる。 +ここでは哲学者の人数を自然数で受け取り、人数分の List Phi と table を一つずつ作成し env を作成している。 +また、最初の哲学者の状態は思考することであるため、next-code には C\_thinking を格納している。 \lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced} -Agda では並列実行を行うことができない．そのため step 単位の実行を一つずつ行うことで -並列実行をしていることとする． +Agda では並列実行を行うことができない。そのため step 単位の実行を一つずつ行うことで +並列実行をしていることとする。 -この際に Env にある List Phi の中身を展開しながら一つずつ行動を処理していく． +この際に Env にある List Phi の中身を展開しながら一つずつ行動を処理していく。 -\lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced} +\lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=code:agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced} -Code \ref{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる． +\coderef{agda-dpp-lfork}が step 実行をした際に哲学者が左側のフォークを取る記述になる。 -左側のフォークを取る際には table の index は pid の次の値になっている． -図 \ref{fig:DPP} を見ると直感的に理解ができる． +左側のフォークを取る際には table の index は pid の次の値になっている。 +\figref{DPP} を見ると直感的に理解ができる。 -最後の哲学者は一番最初のフォークを参照する必要がある． -フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので +最後の哲学者は一番最初のフォークを参照する必要がある。 +フォークの状態を確認し、値が0である場合はフォークがテーブルの上にあるので それを自分の pid に書き換える。次に left-hand を true に書き換えて手に持つ -フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は -状態を変化させずに処理を続ける． -このように左のフォークを取る記述をした． +フォークの状態が0以外、すなわち他の哲学者がその場所のフォークを取得している場合は +状態を変化させずに処理を続ける。 +このように左のフォークを取る記述をした。 -右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る． -比較するべき table の List と哲学者のListは一致しているため，pickup\_lfork のように最後の哲学者が -最初のフォークを参照することもない． +右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る。 +比較するべき table の List と哲学者のListは一致しているため、pickup\_lfork のように最後の哲学者が +最初のフォークを参照することもない。 -似たような形で哲学者がフォークを置く putdown-lfork/rfork を実装した． -思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている． +似たような形で哲学者がフォークを置く putdown-lfork/rfork を実装した。 +思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている。 \section{Gears Agda によるDPPの検証} これまでの実装は一般的なDPPの実装であったため, -Code / Data Gear の実装であった. -ここからは,モデル検査を行うため,Meta Data Gear の定義をし, -それの操作を行う Meta Code Gear の実装を行っていく. +Code / DataGear の実装であった。 +ここからは,モデル検査を行うため,Meta DataGear の定義をし, +それの操作を行う Meta CodeGear の実装を行っていく。 -以下\coderef{dpp-mdg}がMeta Data Gear の定義になる。 +以下\coderef{dpp-mdg}がMeta DataGear の定義になる。 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける -\lstinputlisting[caption=Gears Agda で DPP のモデル検査を行うための Meta Data Gear, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced} +\lstinputlisting[caption=Gears Agda で DPP のモデル検査を行うための Meta DataGear, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced} -この Meta Data Gear の説明をすると, -metadataは状態の分岐数を持っておくnum-brunchがある. -MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)となる。 +この Meta DataGear の説明をすると, +metadataは状態の分岐数を持っておくnum-brunchがある。 +MetaEnv はもとの DataGear を保持するDG(DataGearの省略)となる。 meta には前述したmetadataを持っており, 他には,deadlockしているかのフラグである deadlock , 最後の2つは後に必要になるフラグである。 そのstate が step 実行済みなのかのフラグであるis-step, -そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている. +そのstateがモデル検査済なのかのフラグであるis-doneフラグを持っている。 -MetaEnv2 は1つのstate である MetaEnv の Listを metal で持てる. -加えて今まで実行していた Data Gear を DG で持てる. +MetaEnv2 は1つのstate である MetaEnv の Listを metal で持てる。 +加えて今まで実行していた DataGear を DG で持てる。 -次に Meta Data Gear を作成する Meta Code Gear の説明をする。 +次に Meta DataGear を作成する Meta CodeGear の説明をする。 \begin{enumerate} - \item その状態から分岐できる状態数をカウントする Meta Code Gear - \item Wait List を作成する Meta Code Gear + \item その状態から分岐できる状態数をカウントする Meta CodeGear + \item Wait List を作成する Meta CodeGear \end{enumerate} -以下の \coderef{dpp-mcg-branch} が分岐できる状態数をカウントする Meta Code Gear となる。 +以下の \coderef{dpp-mcg-branch} が分岐できる状態数をカウントする Meta CodeGear となる。 %ここにコードを載せる% -\lstinputlisting[caption=状態の分岐数をカウントする Meta Data Gear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced} +\lstinputlisting[caption=状態の分岐数をカウントする Meta DataGear の定義, label=code:dpp-mcg-branch]{src/dpp-verif/dpp-metacode.agda.replaced} -実際にやっていることは,MetaEnv2 から state を取り出し,分岐を見る関数に遷移させている.その結果の List の length を meta データとしている. +実際にやっていることは,MetaEnv2 から state を取り出し,分岐を見る関数に遷移させている。その結果の List の length を meta データとしている。 -つまり,この Meta Code Gear の実装にあたって新しい実装はほとんど行っていない. +つまり,この Meta CodeGear の実装にあたって新しい実装はほとんど行っていない。 -Wait List の 作成も同じように取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている. +Wait List の 作成も同じように取り出した state を step させて,そこで一致するnext-codeを状態が変わっていないとして Wait List に入れている。 %いちおうコード載せようかな？←棄却されました% -Wait List について,Thinking と Eathing の状態に関しては状態が変わる可能性がある. -これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる.しかし,DPP以外の他のプログラムをモデル検査する際に,一つ一つ next-code の設定を行うのは煩雑であると考えた.そのため,step した際に状態が変化しないものを Wait List にいれた.これと分岐がない場合という条件にて,dead lock を検知する.これにより Meta Code Gear の作成が簡易化された.そのため,Thinking と Eathing のプロセスも Waithing List に入るようになっている. +Wait List について,Thinking と Eathing の状態に関しては状態が変わる可能性がある。 +これを Wait List に入れなければ Wait List のみで dead lock が検知できると考えられる。しかし,DPP以外の他のプログラムをモデル検査する際に,一つ一つ next-code の設定を行うのは煩雑であると考えた。そのため,step した際に状態が変化しないものを Wait List にいれた。これと分岐がない場合という条件にて,dead lock を検知する。これにより Meta CodeGear の作成が簡易化された。そのため,Thinking と Eathing のプロセスも Waithing List に入るようになっている。 -deadlockの検出方法として,上記の2つのMeta Code Gear で作成したmeta データを使用する. +deadlockの検出方法として,上記の2つのMeta CodeGear で作成したmeta データを使用する。 -そして「num-brunchの値が1であり,wait Listの数がプロセス数と一致する」ということは,「その状態から別の状態に遷移することができない」として,この状態をdead lockであると定義した. +そして「num-brunchの値が1であり,wait Listの数がプロセス数と一致する」ということは,「その状態から別の状態に遷移することができない」として,この状態をdead lockであると定義した。 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる。 複雑なことは何もしておらず,単純にstate毎のnum-brunchの値を見て,wait-listの数がプロセス数と一致していた場合に -deadlockのフラグを立ち上げている.これが,Gears Agda におけるアサーションになっている. +deadlockのフラグを立ち上げている。これが,Gears Agda におけるアサーションになっている。 % judge-dead-lock-pのソースコードを貼り付ける -\lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced} +\lstinputlisting[caption=DPP での dead lock を検知する Meta CodeGear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced} % こいつはmetaEnv2を受け取れるように変えないと行けない -ここから前述した通り,State Listを作成する. +ここから前述した通り,State Listを作成する。 -そのまま実行するだけでは無限に実行されるのみで停止しないと思われる. -しかし,分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる. -存在していた場合はそれを追加せず,存在しなかった場合にのみ State を追加する. +そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。 +しかし,分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。 +存在していた場合はそれを追加せず,存在しなかった場合にのみ State を追加する。 Agdaには2つの record が等しいか確かめる関数などは存在せず, -\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する. -こちらはそのまま掲載すると長いので,実際のコードに手を加えて省略している.実際のコードは付録にて参照できる. +\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つずつ一致しているか確認する。 +こちらはそのまま掲載すると長いので,実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。 -\lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced} +\lstinputlisting[caption=重複しているstateを除外する Meta CodeGear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced} % 手を加えているので詳細は付録を参照するように促す -MetaEnv2 を受け取ってその中身の state を比較するが,そこまで展開する必要がある. - loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている. +MetaEnv2 を受け取ってその中身の state を比較するが,そこまで展開する必要がある。 + loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。 -更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し,次のstateの一致を探索するように記述されている. +更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し,次のstateの一致を探索するように記述されている。 実際にstateの一致を見ているのは22行目のeq-env関数で,一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている。 -State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている. -その値が一致している場合には別の値を見て,一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている. -他の値である,lhandやrhandなども eq-pid と同じように記述している. +State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。 +その値が一致している場合には別の値を見て,一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。 +他の値である,lhandやrhandなども eq-pid と同じように記述している。 -これらにて,まだ分岐を見ていない1つのStateの分岐を確かめる. -発生した分岐を step 実行させる. -step実行して作成された state が State Listに存在していないかを確かめる. -これを繰り返すことで State Listを作る. +これらにて,まだ分岐を見ていない1つのStateの分岐を確かめる。 +発生した分岐を step 実行させる。 +step実行して作成された state が State Listに存在していないかを確かめる。 +これを繰り返すことで State Listを作る。 State List に存在している全ての state の分岐を見たということは, -出現するStateを全て網羅することができたと言える. +出現するStateを全て網羅することができたと言える。 -あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる。 +あとは State List を dead lock の検査を行う Meta CodeGear に与えるとどの state が dead lockしているかを検証することができる。 \section{Gears Agda による live lockの検証方法について} -live lockとは,状態が変動しているが,その状態はループしており,実行が進んでいないことを指す. +live lockとは,状態が変動しているが,その状態はループしており,実行が進んでいないことを指す。 -DPPにて例を上げると,(上の哲学者のフローだと) dead lock が発生するため,フローを変更したとする.それは以下のような動作を追加する. +DPPにて例を上げると,(上の哲学者のフローだと) dead lock が発生するため,フローを変更したとする。それは以下のような動作を追加する。 「右手にフォークを持っているが,左手のフォークがすでに取られている場合に右手のフォークを即座に置いて固定時間待つ」 -とする.これで解決すると思われるが,全員が同時に食事をしようとした場合,右手のフォークを取ったり置いたりを永遠に繰り返すことになる. +とする。これで解決すると思われるが,全員が同時に食事をしようとした場合,右手のフォークを取ったり置いたりを永遠に繰り返すことになる。 これを live lock という -つまり,この状態を検知するなら,そのstateが持っているhistoryまで考慮する必要がある.つまり,今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い. +つまり,この状態を検知するなら,そのstateが持っているhistoryまで考慮する必要がある。つまり,今回の場合だとstateのloopができた際にコマンドが一巡しているかを確認すると良い。 -history がloopしていた際に,誰もeathingしていない場合を live lock していると定義する. +history がloopしていた際に,誰もeathingしていない場合を live lock していると定義する。 -今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める.それがloop中に存在しているかを確認することで live lock を検知できる. +今回のはDPPであるためEatingが挙げられているが,他の実装であれば,どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在しているかを確認することで live lock を検知できる。 \section{Gears Agda でのモデル検査の評価} -SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方がコードも長く、制約が多いため難解に思える.しかし,Gears Agda ではプログラムの実装も含んでいる. +SPINで行ったDPPのモデル検査に比べると,Gears Agdaの方がコードも長く、制約が多いため難解に思える。しかし,Gears Agda ではプログラムの実装も含んでいる。 -さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta Code Gear の流れは変化しないため,他のプログラムに適応できることを考えると比較的容易であると言える. +さらに,Gears Agda での実装をしたあとのモデル検査を行う際の Meta CodeGear の流れは変化しないため,他のプログラムに適応できることを考えると比較的容易であると言える。 -加えて,Gears Agda は CbC へコンパイルされ,高速に実行されることを踏まえると,いかに Gears Agda が検証に向いたプログラムであるか理解できる. +加えて,Gears Agda は CbC へコンパイルされ,高速に実行されることを踏まえると,いかに Gears Agda が検証に向いたプログラムであるか理解できる。 % この評価の話はまとめでしたほうがいいかもね？
--- a/Paper/tex/future.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/future.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,24 +1,24 @@ \chapter{まとめ} -本論文では，Agda による CbCの検証方法と Gears Agda による -Left Learning Red Black Tree の実装について述べた． -したがって，Gears Agda で再起処理と再代入を含んだ -複雑なアルゴリズムも記述できる事が判明した． +本論文では、Agda による CbCの検証方法と Gears Agda による +Left Learning Red Black Tree の実装について述べた。 +したがって、Gears Agda で再起処理と再代入を含んだ +複雑なアルゴリズムも記述できる事が判明した。 今回の研究中に複雑なアルゴリズムを Gears Agda にて実装することで -得られた知見は，今後の研究で大いに役立つと考える． +得られた知見は、今後の研究で大いに役立つと考える。 -今後の課題として，検証を行う事が挙げられる． -検証には，Meta Code Gear が Pre / Post Condition の条件を -満たしているのか比較を行い，Hoare Logicに当てはめる事． -そして接続された条件の接続と健全性の証明を行う必要がある． -しかし，Imple を用いた Hoare Logic による証明は， -While Loop でも かなり長いコードになっていた． +今後の課題として、検証を行う事が挙げられる。 +検証には、Meta CodeGear が Pre / Post Condition の条件を +満たしているのか比較を行い、Hoare Logicに当てはめる事。 +そして接続された条件の接続と健全性の証明を行う必要がある。 +しかし、Imple を用いた Hoare Logic による証明は、 +While Loop でも かなり長いコードになっていた。 これで Left Learning Red Black Tree の検証を -行うのは難しいため，別の手法を模索することも念頭に入れる． +行うのは難しいため、別の手法を模索することも念頭に入れる。 -展望としては，Gears Agda コードから CbC コードの変換をしたい． -Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが， -CbC はC言語とアセンブラの中間に位置しているため，コーディングはさらに困難である． -そのため，Gears Agdaのコードを CbC に変換できるようにしたい． -これができるようになれば，CbC での記述も Agda での証明も容易になると考えている． +展望としては、Gears Agda コードから CbC コードの変換をしたい。 +Gears Agda は Agda の記述方法が特殊である事がコーディングを複雑にしているが、 +CbC はC言語とアセンブラの中間に位置しているため、コーディングはさらに困難である。 +そのため、Gears Agdaのコードを CbC に変換できるようにしたい。 +これができるようになれば、CbC での記述も Agda での証明も容易になると考えている。
--- a/Paper/tex/hoare.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/hoare.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,31 +1,33 @@ \chapter{Gears Agda による定理証明} -先行研究\cite{ryokka-sigos}では,Gears Agda ではないプログラムの Hoare Logic による検証\cite{agda2-hoare}を参考にそれを Gears Agda に適応して while loop の検証を行っていた\cite{cr-ryukyu}. -本研究では,invariant というプログラムの不変条件を定義し,それを検証することで,比較的容易に検証を行うことができるようになった(本章2節) -本章では Gears Agda による定理証明の方法について説明する. +先行研究\cite{ryokka-sigos}では,Gears Agda ではないプログラムの Hoare Logic による検証\cite{agda2-hoare}を参考にそれを Gears Agda に適応して while loop の検証を行っていた\cite{cr-ryukyu}。 +本研究では,Invariant というプログラムの不変条件を定義し,それを検証することで,比較的容易に検証を行うことができるようになった(本章2節) +本章では Gears Agda による定理証明の方法について説明する。 \section{Hoare Logic} -Hoare Logic\cite{hoare} とは C.A.R Hoare， -R.W Floyd が考案したプログラムの検証の手法である． -これは，「プログラムの事前条件(P)が成立しているとき， +Hoare Logic\cite{hoare} とは C.A.R Hoare、 +R.W Floyd が考案したプログラムの検証の手法である。 +これは、「プログラムの事前条件(P)が成立しているとき、 コマンド(C)実行して停止すると事後条件(Q)が成り立つ」 -というものである。これはCbCの実行を継続するという性質に非常に相性が良い． -Hoare Logic を表記すると以下のようになる． +というものである。これはCbCの実行を継続するという性質に非常に相性が良い。 +Hoare Logic を表記すると以下のようになる。 $$ \{P\}\ C \ \{Q\} $$ -この3つ組は Hoare Triple と呼ばれる． +この3つ組は Hoare Triple と呼ばれる。 -Hoare Triple の事後条件を受け取り， -異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく． +Hoare Triple の事後条件を受け取り、 +異なる条件を返す別の Hoare Triple を繋げることでプログラムを記述していく。 -Hoare Logic の検証では， -「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である． -これらを満たし， -事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる． +Hoare Logic の検証では、 +「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。 +これらを満たし、 +事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 -\subsection{Hoare Logic による Code Gear の検証手法 } +\section{Invariant を用いた Hoare Logic による検証の方法 } -図\ref{fig:meta-cgdg}を用いて Agda にて Hoare Logic による Code Gear を検証する流れを説明する． -input DataGear が Hoare Logic上の Pre Condition(事前条件)となり， -output DataGear が Post Conditionとなる． -各DataGear が Pre / Post Condition を満たしているかの検証は， -各 Condition を Meta DataGear で定義し， -条件を満たしているのかをMeta CodeGear で検証する． +\figref{meta-cgdg}を用いて Agda にて Hoare Logic による CodeGear を検証する流れを説明する。 +input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、 +output DataGear が Post Conditionとなる。 +各DataGear が Pre / Post Condition を満たしているかの検証は、 +各 Condition を Meta DataGear で定義し、 +条件を満たしているのかをMeta CodeGear で検証する。 + +この際、検証する DataGear はプログラムの不変条件となり、これを Invariant と呼ぶ。 \ No newline at end of file
--- a/Paper/tex/intro.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/intro.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,27 +1,27 @@ \chapter{Gears Agda でのプログラムの検証} OSやアプリケーションの信頼性の向上は重要である。 -信頼性を向上するための手段として,プログラムを検証する事が挙げられる. +信頼性を向上するための手段として、ログラムを検証する事が挙げられる。 -しかし,仕様の形式化とその検証には膨大なコストを要する． -そのため，他のプログラミング言語と比べて検証に適している Gears Agda を使用する． -Gears Agda とは当研究室で開発している Continuation based C \cite{cbc-gcc}(以下CbC) の概念を取り入れた記法で記述された Agda \cite{agda} のことである． +しかし、様の形式化とその検証には膨大なコストを要する。 +そのため、他のプログラミング言語と比べて検証に適している Gears Agda を使用する。 +Gears Agda とは当研究室で開発している Continuation based C \cite{cbc-gcc}(以下CbC) の概念を取り入れた記法で記述された Agda \cite{agda} のことである。 -通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する． -この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了し， -メインルーチンに戻る際にスタックしていた環境に戻す流れとなる． -CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができる。そのため、環境をスタックに保持しない． -したがって関数の実行では暗黙な環境が存在せず，関数は受け取った引数のみを使用する． -この関数の単位を Code Gear と呼び，Code Gearの引数を Data Gear と呼んでいる． +通常のプログラミング言語では関数を実行する際にメインルーチンからサブルーチンに遷移する。 +この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了し、 +メインルーチンに戻る際にスタックしていた環境に戻す流れとなる。 +CbCの場合はサブルーチンコールの際にアセンブラでいう jmp命令 により関数遷移を行うことができる。そのため、環境をスタックに保持しない。 +したがって関数の実行では暗黙な環境が存在せず、関数は受け取った引数のみを使用する。 +この関数の単位を CodeGear と呼び、CodeGearの引数を DataGear と呼んでいる。 -これにより検証を Code Gear 単位に分割することができ，比較的容易に検証を行えるようになっている． +これにより検証を CodeGear 単位に分割することができ、比較的容易に検証を行えるようになっている。 -また、先行研究\cite{ryokka-sigos}では,Gears Agda での並列実行の検証について課題が残っていた. -並列実行の検証を定理証明で行うには,考慮する状態の数が膨大になり困難である. -そのため,Gears Agda でモデル検査\cite{EdmundM}を行うことでこの課題に対応する. +また、先行研究\cite{ryokka-sigos}では、ears Agda での並列実行の検証について課題が残っていた。 +並列実行の検証を定理証明で行うには、慮する状態の数が膨大になり困難である。 +そのため、ears Agda でモデル検査\cite{EdmundM}を行うことでこの課題に対応する。 -CbCの継続の概念はモデル検査とも相性がよい．\cite{ikkun-master} -CbCが末尾関数呼び出しであるため Code Gear をそのまま -モデルの edge として定義することが可能である． +CbCの継続の概念はモデル検査とも相性がよい。\cite{ikkun-master} +CbCが末尾関数呼び出しであるため CodeGear をそのまま +モデルの edge として定義することが可能である。 -これらのことから,本論文では,Gears Agda での定理証明とモデル検査について述べる。 \ No newline at end of file +これらのことから、論文では、ears Agda での定理証明とモデル検査について述べる。 \ No newline at end of file
--- a/Paper/tex/main.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/main.tex Thu Feb 02 20:52:51 2023 +0900 @@ -2,14 +2,14 @@ ここまでで Gears Agda を用いたアルゴリズム適用可否探索の方法を示した. これのアルゴリズムに当たる部分をニューラルネットワークの中間層の計算式に置き換えて考える. -現在,ハードウェア技術,機械学習技術の両方の進歩により +現在、ードウェア技術、械学習技術の両方の進歩により ニューラルネットワークの中間層が増加しても Residual Block や Dense Block などの勾配を伝搬する経路を確保することで 勾配消失問題は発生しなくなった.\cite{DBLP:journals/corr/HeZRS15}\cite{DBLP:journals/corr/HuangLW16a} -しかし,中間層が増加していることによるモデルサイズの肥大化や計算量の増加からは逃れられない. +しかし、間層が増加していることによるモデルサイズの肥大化や計算量の増加からは逃れられない. -この問題に対して,複数の中間層をより少ない数の中間層で置き換えることができないか探索を行う. -加えて,考案した新規の計算式を考慮するようにし,その妥当性を考慮したり, +この問題に対して、数の中間層をより少ない数の中間層で置き換えることができないか探索を行う. +加えて、案した新規の計算式を考慮するようにし、の妥当性を考慮したり, 現在扱っていない数式自体を組み合わせの全探索によって構築し模索することもできると考える. \subsection{中間層の圧縮と新しいレイヤー計算式の開発} @@ -20,11 +20,11 @@ これにより複数のレイヤーの組み合わせと等しい計算をしている それ以下の組み合わせで実現できないかを探索する. -完全に等しい計算式を探索するのが難しい場合は,ある程度一致している +完全に等しい計算式を探索するのが難しい場合は、る程度一致している 計算を出せるようにしてもよいと考えている. -また,レイヤーの計算式を格納している部分に,新しい計算式を -加えることで,新しいレイヤーの計算式を開発できるとも考えている. +また、イヤーの計算式を格納している部分に、しい計算式を +加えることで、しいレイヤーの計算式を開発できるとも考えている. -さらに,その新規で追加する計算式も探索により作成することも +さらに、の新規で追加する計算式も探索により作成することも できると想定している.
--- a/Paper/tex/rbt_imple.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/rbt_imple.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,14 +1,14 @@ \chapter{Red Black Tree の実装} -Left Learning Red Black Tree の実装において， +Left Learning Red Black Tree の実装において、 通常の言語であれば再起処理を用いて実装を行える部分を -継続にて実行可能なように変更する必要がある． -本節では，この課題に対して Gears Agda での -Left Learning Red Black Tree の実装方法について述べる． +継続にて実行可能なように変更する必要がある。 +本節では、この課題に対して Gears Agda での +Left Learning Red Black Tree の実装方法について述べる。 \section{Gears Agda での Red Black Tree の 記述} -Gears Agda にて Red Black Tree を実装する際の手順を， -下\figref{rbt_imple}を参考に説明する． +Gears Agda にて Red Black Tree を実装する際の手順を、 +下\figref{rbt_imple}を参考に説明する。 \begin{figure}[H] \begin{center} @@ -18,103 +18,103 @@ \label{rbt_imple} \end{figure} -41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する． -まず Root node である 59 と比較した際に，41はそれより小さい． -この際，left node に遷移するが，CbC では再起処理が行えないため，listに保持していく． -順々に辿っていき，対象の場所に到達すると insert / delete を行う． -その後はlistからnodeを取り出し，結合することで Left Leaning Red Black Tree の操作を行う． +41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。 +まず Root node である 59 と比較した際に、41はそれより小さい。 +この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。 +順々に辿っていき、対象の場所に到達すると insert / delete を行う。 +その後はlistからnodeを取り出し、結合することで Left Leaning Red Black Tree の操作を行う。 -\subsection{定義した Data Gear の記述} +\subsection{定義した DataGear の記述} -Left Learning Red Black Tree の記述の際に， Code Gear -に渡している Data Gear である Env の記述を \coderef{env_imple} に示す． +Left Learning Red Black Tree の記述の際に、 CodeGear +に渡している DataGear である Env の記述を \coderef{env_imple} に示す。 \lstinputlisting[label=env_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=13, lastline=39] {src/agda/rbt_t.agda} -箇条書きにてそれぞれについて解説を行う． +箇条書きにてそれぞれについて解説を行う。 \begin{itemize} -\item col: 色のことで，red と black の data 型で記述し，パターンマッチを行う． -\item node: その名の通り node に格納されている値を保存する． 色と自然数が入る -\item tree: tree の構造 を保存する．ここで node と x / right tree を持つ +\item col: 色のことで、red と black の data 型で記述し、パターンマッチを行う。 +\item node: その名の通り node に格納されている値を保存する。 色と自然数が入る +\item tree: tree の構造 を保存する。ここで node と x / right tree を持つ \item rbt: 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する -\item Env: rbt 以外に追加や削除を行う対象となる値と， rbtを保存できる List を持つ Data Gear +\item Env: rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ DataGear \end{itemize} \subsection{目的の node まで辿る Gears Agda} -上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる． -例は insert を行う場合の記述となる． +上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。 +例は insert を行う場合の記述となる。 \lstinputlisting[label=insert_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=157, lastline=166] {src/agda/rbt_t.agda} -ソースコードの解説をする．上から3行はコメントで，この関数で行っていることを doに， -next / exit では4章で述べた次の関数遷移先を記載している． +ソースコードの解説をする。上から3行はコメントで、この関数で行っていることを doに、 +next / exit では4章で述べた次の関数遷移先を記載している。 -5行目にて withを使用することで vart のパターンマッチを行っている． -vart が bt-empty である場合に 6行目が動作する． -bt-empty であれば node の一番下であるため， -varn を tree の値として insert して exit に遷移する． +5行目にて withを使用することで vart のパターンマッチを行っている。 +vart が bt-empty である場合に 6行目が動作する。 +bt-empty であれば node の一番下であるため、 +varn を tree の値として insert して exit に遷移する。 -7行目は vart が bt-empty ではないパターンの動作を記述している． -ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い， -再度パターンマッチを行う． +7行目は vart が bt-empty ではないパターンの動作を記述している。 +ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い、 +再度パターンマッチを行う。 -8行目は比較した結果，同値だった場合であり，そのままexitに遷移している． +8行目は比較した結果、同値だった場合であり、そのままexitに遷移している。 -9行目は入力の値 varn の方が小さい場合を指している． -vart に left tree を入れ，varl には 現在の tree から left treeを除いた -treeを追加している．それを next に遷移させている． +9行目は入力の値 varn の方が小さい場合を指している。 +vart に left tree を入れ、varl には 現在の tree から left treeを除いた +treeを追加している。それを next に遷移させている。 -10行目は入力の値 varn の方が大きい場合を指している． -9行目とは逆に，vart に right tree を入れ，varl には 現在の tree から right treeを除いた -treeを追加している．それをまたnext に遷移させている． +10行目は入力の値 varn の方が大きい場合を指している。 +9行目とは逆に、vart に right tree を入れ、varl には 現在の tree から right treeを除いた +treeを追加している。それをまたnext に遷移させている。 -以上の手順により，目的の node まで辿っている． +以上の手順により、目的の node まで辿っている。 \subsection{目的の node まで辿った後の Gears Agda} -目的の node にたどり着いた後，List に格納された tree と vart の結合を行う． -Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる． +目的の node にたどり着いた後、List に格納された tree と vart の結合を行う。 +Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる。 \lstinputlisting[label=mearge_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=145, lastline=155] {src/agda/rbt_t.agda} -ソースコードの解説をする． -5行目にて with を使用して varl についてパターンマッチを行っている． +ソースコードの解説をする。 +5行目にて with を使用して varl についてパターンマッチを行っている。 -6行目が varl に何も入っていない場合で，実行終了のため exitに遷移している． +6行目が varl に何も入っていない場合で、実行終了のため exitに遷移している。 -7行目は varl に何か入っていた場合で，ここでは varl に入っているものが -何であるのか8行目と合わせてパターンマッチを行っている． -ここでは varl に入っていたものが bt-empty であった場合について記述されている． -bt-emptyが入ってくることは実装上ありえないので，exitに遷移することで強制終了している． +7行目は varl に何か入っていた場合で、ここでは varl に入っているものが +何であるのか8行目と合わせてパターンマッチを行っている。 +ここでは varl に入っていたものが bt-empty であった場合について記述されている。 +bt-emptyが入ってくることは実装上ありえないので、exitに遷移することで強制終了している。 -8行目では varl に入っていたものが bt-empty ではなかった場合で， -それをxtreeと命名している． -ここで vart に入っている値と xtree に入っている値を比較を行い， -さらにパターンマッチを行う． +8行目では varl に入っていたものが bt-empty ではなかった場合で、 +それをxtreeと命名している。 +ここで vart に入っている値と xtree に入っている値を比較を行い、 +さらにパターンマッチを行う。 -9行目が入っている値と同じ値であった場合で， -特に操作する必要がないので vart に xtree を入れ， -varl を一つ進める． +9行目が入っている値と同じ値であった場合で、 +特に操作する必要がないので vart に xtree を入れ、 +varl を一つ進める。 -10行目は vartが大きい場合で， -varnに xtree の値を入れ， +10行目は vartが大きい場合で、 +varnに xtree の値を入れ、 xtree の right tree に 現在のvart を入れたものを vartにして -varlを一つ進めている． +varlを一つ進めている。 -11行目は vartが小さい場合で， -10行目と逆のことをしている． -varnに xtree の値を入れ， +11行目は vartが小さい場合で、 +10行目と逆のことをしている。 +varnに xtree の値を入れ、 xtree の left tree に 現在のvart を入れたものを vartにして -varlを一つ進めている． +varlを一つ進めている。 -以上の組み合わせを行い， +以上の組み合わせを行い、 Gears Agda にて 再起処理を使わず に Left Learning Red Black Tree の insert / delete を -記述した． +記述した。 -% 以上のように Tree の基本操作である insert, find, delete の実装を行った． +% 以上のように Tree の基本操作である insert, find, delete の実装を行った。
--- a/Paper/tex/rbt_intro.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/rbt_intro.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,20 +1,20 @@ \chapter{Red Black Tree} -実装を行う Red Black Tree の説明を行う． -Red Black Tree は 木構造の基本操作である Insert(挿入)，Delete(削除)，Search(検索)の -いずれに置いても最悪実行時間が $O(log \: n)$であり，データ構造のうちで最善のものの一つである． -そのため，実用的なデータ構造として知られている． +実装を行う Red Black Tree の説明を行う。 +Red Black Tree は 木構造の基本操作である Insert(挿入)、Delete(削除)、Search(検索)の +いずれに置いても最悪実行時間が $O(log \: n)$であり、データ構造のうちで最善のものの一つである。 +そのため、実用的なデータ構造として知られている。 \section{Tree} -Tree (木構造)とは，非常に有用なデータ構造である． -\figref{tree}の○の部分を node (節) と呼び，top node を root(根) と呼ぶ． -特に，根を持つ木構造のことを強調して，Rooted Tree (根付き木) と呼ぶ事がある． +Tree (木構造)とは、非常に有用なデータ構造である。 +\figref{tree}の○の部分を node (節) と呼び、top node を root(根) と呼ぶ。 +特に、根を持つ木構造のことを強調して、Rooted Tree (根付き木) と呼ぶ事がある。 \section{Binary Tree} 各 node からすぐ下に辺で結ばれている node を -その node の child またはson (子あるいは子供)と呼ぶ． -child 側から上の辺を parent (親) と呼ぶ． -\figref{bt}のように，各 node が持つ child が高々2つである Tree を Binary Tree (2分木)と呼ぶ． +その node の child またはson (子あるいは子供)と呼ぶ。 +child 側から上の辺を parent (親) と呼ぶ。 +\figref{bt}のように、各 node が持つ child が高々2つである Tree を Binary Tree (2分木)と呼ぶ。 \begin{figure}[htbp] \begin{minipage}{0.5\hsize} @@ -34,7 +34,7 @@ \end{figure} \section{Binary Search Tree} -Rooted Binary Tree に対して， 以下の制約を持つものを，Binary Search Tree と呼ぶ． +Rooted Binary Tree に対して、 以下の制約を持つものを、Binary Search Tree と呼ぶ。 $左側の子孫にある要素 < 親 < 右側の子孫にある要素$ @@ -49,19 +49,19 @@ \end{figure} \section{RedBlackTree} -RedBlackTree (または赤黒木)とは平衡2分探索木の一つである． -2分探索木の点にランクという概念を追加し，そのランクの違いを赤と黒の色で分け， +RedBlackTree (または赤黒木)とは平衡2分探索木の一つである。 +2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、 以下の定義に基づくように -木を構成した物である．図では省略しているが，値を持っている点の下に黒色の空の葉があり， -それが外点となる． +木を構成した物である。図では省略しているが、値を持っている点の下に黒色の空の葉があり、 +それが外点となる。 \begin{enumerate} - \item 各点は赤か黒の色である． - \item 点が赤である場合の親となる点の色は黒である． - \item 外点(葉．つまり一番下の点)は黒である． - \item 任意の点から外点までの黒色の点はいずれも同数となる． + \item 各点は赤か黒の色である。 + \item 点が赤である場合の親となる点の色は黒である。 + \item 外点(葉。つまり一番下の点)は黒である。 + \item 任意の点から外点までの黒色の点はいずれも同数となる。 \end{enumerate} -参考となる\figref{rbt}を以下に示す．上記の定義を満たしていることが分かる． +参考となる\figref{rbt}を以下に示す。上記の定義を満たしていることが分かる。 \begin{figure}[H] \begin{center} @@ -72,18 +72,18 @@ \end{figure} \section{Left Learning Red Black Tree} -Left Learing Red Black Tree とは Red Black Tree の変形である． -Red Black Tree の 仕様を満たしながら，実装が容易である． +Left Learing Red Black Tree とは Red Black Tree の変形である。 +Red Black Tree の 仕様を満たしながら、実装が容易である。 \figref{rbt}に入っていた値を Left Learning Red Black Tree に適応した場合を -\figref{llrbt}に示す． +\figref{llrbt}に示す。 Left Learning Red Black Tree では赤色の node は parent から見て -左の node にしか 現れない Red Black Tree となる． -これにより，パターンマッチの分岐を減らす事ができ，実装が容易になる． +左の node にしか 現れない Red Black Tree となる。 +これにより、パターンマッチの分岐を減らす事ができ、実装が容易になる。 -本来の Red Black Tree の実装は困難であるため， +本来の Red Black Tree の実装は困難であるため、 本論では Red Black Tree の仕様を満たしている -Left Learning Red Black Tree を検証する． +Left Learning Red Black Tree を検証する。 \begin{figure}[H] \begin{center}
--- a/Paper/tex/rbt_verif.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/rbt_verif.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,64 +1,64 @@ \chapter{Left Learning Red Black Tree の検証} -本章では，Left Learning Red Black Tree の +本章では、Left Learning Red Black Tree の 検証方法について述べる -\section{Meta Data Gearの記述} -検証するにあたり，Meta Deta Gear を作成し Pre / Post Condition と -比較することで Hoare Triple に当てはめることは第5章で前述した． -\subsection{大小関係を検証する Meta Data Gear} -Red Black Tree は Binary Search Tree の 定義を持っているので， -parent から見て left node には parent の値より小さい値が， -right node には大きい値が入る．これを検証する必要がある． +\section{Meta DataGearの記述} +検証するにあたり、Meta Deta Gear を作成し Pre / Post Condition と +比較することで Hoare Triple に当てはめることは第5章で前述した。 +\subsection{大小関係を検証する Meta DataGear} +Red Black Tree は Binary Search Tree の 定義を持っているので、 +parent から見て left node には parent の値より小さい値が、 +right node には大きい値が入る。これを検証する必要がある。 -大小関係を検証するにあたり，Fresh List を用いた検証手法が考えられた． -Fresh Listの記述を\coderef{fresh}に示す． -% ソースコードを載せる． +大小関係を検証するにあたり、Fresh List を用いた検証手法が考えられた。 +Fresh Listの記述を\coderef{fresh}に示す。 +% ソースコードを載せる。 \lstinputlisting[label=fresh, caption=Fresh List の定義, firstline=47,lastline=49] {src/agda/_fresh.agda} -これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す． +これを用いて Frash List への定数の insert を\coderef{fresh-test}に示す。 \lstinputlisting[label=fresh-test, caption=Fresh List への定数のinsert, firstline=10,lastline=15] {src/agda/fresh_test.agda} -Fresh Listは一つの値に対して，それより後の値との大小関係の証明が入っている． -そのため，正確性が増すが，関数内でFresh List への insert は困難であったため， +Fresh Listは一つの値に対して、それより後の値との大小関係の証明が入っている。 +そのため、正確性が増すが、関数内でFresh List への insert は困難であったため、 証明付き Data 構造を持った List を \coderef{list_v} -のように定義した． +のように定義した。 \lstinputlisting[label=list_v, caption=証明付き Data 構造を持った List,firstline=12,lastline=30] {src/agda/rbt_varif.agda} -証明付き Data 構造を持った List の定義は right-List で行っている． -List の Top と比較した際に， -Topの値より大きい値でなければ insert できない． -加えて insert できた値が Top より大きい事を示す証明も持つ事ができる． +証明付き Data 構造を持った List の定義は right-List で行っている。 +List の Top と比較した際に、 +Topの値より大きい値でなければ insert できない。 +加えて insert できた値が Top より大きい事を示す証明も持つ事ができる。 -mutual は 以下の記述全てに対して掛かっている． -これは right-List の定義の中で，top-r を呼び出しており， -top-r は定義の部分で right-List を使用している． -したがって相互呼び出しとなっている． -Agdaは 逐次処理であるため，プログラムの上に宣言してある関数や型しか使用できない． -mutual を掛けることで，プログラムの下で宣言している関数や型を使用する事ができる． +mutual は 以下の記述全てに対して掛かっている。 +これは right-List の定義の中で、top-r を呼び出しており、 +top-r は定義の部分で right-List を使用している。 +したがって相互呼び出しとなっている。 +Agdaは 逐次処理であるため、プログラムの上に宣言してある関数や型しか使用できない。 +mutual を掛けることで、プログラムの下で宣言している関数や型を使用する事ができる。 -right-List の定義は，何も入っていない場合は right-List で停止するようにしている． -List に一つしか値が入っていない場合は，証明付き Data 構造を持つ必要がない． -そのため特記して記述している． -List に他の値が入っている場合は，top とその次の値との比較を証明を持っている． +right-List の定義は、何も入っていない場合は right-List で停止するようにしている。 +List に一つしか値が入っていない場合は、証明付き Data 構造を持つ必要がない。 +そのため特記して記述している。 +List に他の値が入っている場合は、top とその次の値との比較を証明を持っている。 -top-r は Listに入っている Top の値を持ってくる関数を記述している． -insert-r は right-List に 値を insert するための関数で， -right-List の top と入れる引数を比較し， +top-r は Listに入っている Top の値を持ってくる関数を記述している。 +insert-r は right-List に 値を insert するための関数で、 +right-List の top と入れる引数を比較し、 inserする際は値とその証明の両方を持つ事で 証明付き Data 構造を -持った List となっている． +持った List となっている。 -これを Left Learning Red Black Tree の 仕様を満たすように， -全てに対して行う． -その後，条件が接続されているのかを検証したのち，健全性について示す事で -Hoare Logic による検証ができる． +これを Left Learning Red Black Tree の 仕様を満たすように、 +全てに対して行う。 +その後、条件が接続されているのかを検証したのち、健全性について示す事で +Hoare Logic による検証ができる。 %\subsection{Black node の数え上げ} -%他にも，Left Learning Red Brack Tree の black node の数え上げを記述した． +%他にも、Left Learning Red Brack Tree の black node の数え上げを記述した。 -%\subsection{Meta Data Gear の作成} +%\subsection{Meta DataGear の作成}
--- a/Paper/tex/spec.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/spec.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,31 +1,31 @@ \section{検証手法} -本章では検証する際の手法を説明する． -CodeGear の引数となる DataGear が事前条件となり， -それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する． -その後，さらに事後条件となる DetaGear も Meta Gears にて検証する． -これらを用いて Hoare Logic によりプログラムの検証を行いたい． +本章では検証する際の手法を説明する。 +CodeGear の引数となる DataGear が事前条件となり、 +それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 +その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 +これらを用いて Hoare Logic によりプログラムの検証を行いたい。 \subsection{CbC記法で書くagda} -CbCプログラムの検証をするに当たり，AgdaコードもCbC記法で記述を行う．つまり継続渡しを用いて記述する必要がある． -\coderef{agda-cg}が例となるコードである． +CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 +\coderef{agda-cg}が例となるコードである。 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda} -前述した加算を行うコードと比較すると，不定の型 (t) により継続を行なっている部分が見える． -これがAgdaで表現された CodeGear となる． +前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。 +これがAgdaで表現された CodeGear となる。 \subsection{agda による Meta Gears} -通常の Meta Gears はノーマルレベルの CodeGear， DataGear では扱えないメタレベルの計算を扱う単位である． -今回はその Meta Gears をAgdaによる検証の為に用いる． +通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 +今回はその Meta Gears をAgdaによる検証の為に用いる。 \begin{itemize} \item Meta DataGear \mbox{}\\ - Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる． - これを用いることで，仕様となる制約条件を記述することができる． + Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 + これを用いることで、仕様となる制約条件を記述することができる。 \item Meta CodeGear\mbox{}\\ Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear - である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 - す CodeGear である．故に，Meta CodeGear は Agda で記述した CodeGear の検証そのものである + である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 + す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである \end{itemize}
--- a/Paper/tex/spin_dpp.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/spin_dpp.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,25 +1,25 @@ \chapter{Gears Agda によるモデル検査} 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが -できる。しかし、専門的な知識が多く難易度が高いという欠点がある． -加えて,CbCでは並列処理も実行できる\cite{parusu-master}が, -並列処理を定理証明するには検証する状態が膨大になり困難である. -そのため,並列処理はモデル検査にて検証する方が良い. +できる。しかし、専門的な知識が多く難易度が高いという欠点がある。 +加えて、 +並列処理を定理証明するには検証する状態が膨大になり困難である。 +そのため、 \section{モデル検査とは} -モデル検査 (Model Cheking) とは,検証手法のひとつである. +モデル検査 (Model Cheking) とは,検証手法のひとつである。 これはプログラムが入力に対して仕様を満たした動作を -行うことを網羅的に検証することを指す． -しかし,モデル検査と定理証明を比較した際に，モデル検査は入力が無限になる -状態爆発が起こり得るという問題がある． -実際にモデル検査で行うことは,検証したい内容の時相理論式 $\varphi$ を作り,対象のシステムの初期状態 s のモデル M があるとき,M, s が $\varphi$ を満たすかを調べる. +行うことを網羅的に検証することを指す。 +しかし,モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる +状態爆発が起こり得るという問題がある。 +実際にモデル検査で行うことは,検証したい内容の時相理論式 $\varphi$ を作り,対象のシステムの初期状態 s のモデル M があるとき,M, s が $\varphi$ を満たすかを調べる。 \section{Dining Philosophers Problem} 今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP) -を用いることとした． -DPP とは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題 -である． +を用いることとした。 +DPP とは資源共有問題であり、モデル検査をする際に挙げられる代表的な問題 +である。 -DPPのストーリーを図 \ref{fig:DPP} に示している． +DPPのストーリーを\figref{DPP} に示している。 \begin{figure}[htpb] \begin{center} @@ -29,41 +29,41 @@ \label{fig:DPP} \end{figure} -したがって，哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる． +したがって、哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる。 \begin{enumerate} \item しばらくの間思考を行う \item 食事をするために右のフォークを取る - \item 右のフォークを取ったら，次は左のフォークを取る - \item 両方のフォークを取ったら，しばらく食事をする + \item 右のフォークを取ったら、次は左のフォークを取る + \item 両方のフォークを取ったら、しばらく食事をする \item 思考に戻るために左手に持っているフォークをテーブルに置く \item 左手のフォークを置いたあとは右のフォークをテーブルに置く \end{enumerate} -この際，すべての哲学者が同時に右のフォークを取った場合のことを考える． -すべての哲学者はフォークを持っている．次に哲学者は左のフォークを取ろうと -する．しかしフォークは哲学者の人数と同じ数だけ存在しているため， -テーブルの上にフォークはすでにひとつも存在しない． +この際、すべての哲学者が同時に右のフォークを取った場合のことを考える。 +すべての哲学者はフォークを持っている。次に哲学者は左のフォークを取ろうと +する。しかしフォークは哲学者の人数と同じ数だけ存在しているため、 +テーブルの上にフォークはすでにひとつも存在しない。 すべての哲学者は左のフォークを取ろうとするが -誰も右のフォークを置くことがないため，すべての哲学者の動作がこの状態で止まる．（dead lock） -これが起こることを Gears Agda で検出したい． +誰も右のフォークを置くことがないため、すべての哲学者の動作がこの状態で止まる。（dead lock） +これが起こることを Gears Agda で検出したい。 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない -SPIN(Simple Promela INterpreter) \cite{spin}とは一般的にモデル検査に使用されるツールである.これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し,モデル検査を行うことができる. +SPIN(Simple Promela INterpreter) \cite{spin}とは一般的にモデル検査に使用されるツールである。これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し,モデル検査を行うことができる。 -今回 Gears Agda でのモデル検査と比較するために,SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる. +今回 Gears Agda でのモデル検査と比較するために,SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。 \lstinputlisting[caption= SPINにてDPPをモデル検査する際のコードの一部 , label=code:spin-dpp]{src/dpp-verif/spin.pml} -コードを簡単に説明する.哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている. -forkの状態を配列で管理している.0 である状態が誰もそのforkを持っていない状態である.ここでは,5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている. +コードを簡単に説明する。哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている。 +forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは,5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。 -左手のフォークを取る動作も同じように記述する. -SPINではこのコードを元にプログラムが取りうる状態全てを網羅し,モデル検査を行うことができる. +左手のフォークを取る動作も同じように記述する。 +SPINではこのコードを元にプログラムが取りうる状態全てを網羅し,モデル検査を行うことができる。 -\figref{DPP-model}はこのPromelaから作成された状態遷移図になる. -SPINではコードからプログラムの状態遷移図を出力することができる他,プログラムのstep実行など幅広くモデル検査を行うことができる. +\figref{DPP-model}はこのPromelaから作成された状態遷移図になる。 +SPINではコードからプログラムの状態遷移図を出力することができる他,プログラムのstep実行など幅広くモデル検査を行うことができる。 \begin{figure}[htpb] \begin{center}
--- a/Paper/tex/thanks.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/thanks.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,11 +1,11 @@ \chapter*{謝辞} \addcontentsline{toc}{chapter}{謝辞} -本研究の遂行,本論文の作成にあたり,御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します. -共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します. -私の研究において苦楽を共にした Manjaro Linux とその開発者には頭が上がりません. -さらに,ゼミの前においしいご飯で元気づけてくれた Hally's Cafe に感謝しております. -最後に, 有意義な時間を共に過ごした理工学研究科工学専攻の学友,並びに物心両面で支えてくれた家族に深く感謝致します. +本研究の遂行、 +共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。 +私の研究において苦楽を共にした Manjaro Linux とその開発者には頭が上がりません。 +さらに、 Hally's Cafe に感謝しております。 +最後に、有意義な時間を共に過ごした理工学研究科工学専攻の学友、 \begin{flushright} 2023年 3月 \\ 上地悠斗
--- a/Paper/tex/tree_desc.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/tree_desc.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,18 +1,18 @@ \section{Gears Agda における Binary Tree の検証} -ここでは Gears Agda にて再帰的なデータ構造を検証する例として， -Binary Tree \cite{rbtree} を実装・検証する． +ここでは Gears Agda にて再帰的なデータ構造を検証する例として、 +Binary Tree \cite{rbtree} を実装・検証する。 \subsection{Gears Agda における木構造の設計} -本研究では，Gears Agda にて Binary Tree の検証を行う際に， -Agda が変数に対して再代入を許していないことが問題になってくる． +本研究では、Gears Agda にて Binary Tree の検証を行う際に、 +Agda が変数に対して再代入を許していないことが問題になってくる。 -そのため下図 \ref{fig:rbt-stack} のように，木構造の root から leaf に 辿る際に見ているnodeから -下の tree をそのまま stack に持つようにする． +そのため下\figref{rbt-stack} のように、木構造の root から leaf に 辿る際に見ているnodeから +下の tree をそのまま stack に持つようにする。 -そして insert や delete を行った後に stack から tree を取り出し， -元の木構造を再構築 していきながら rootへ戻る． +そして insert や delete を行った後に stack から tree を取り出し、 +元の木構造を再構築 していきながら rootへ戻る。 \begin{figure}[htpb] \begin{center} @@ -21,78 +21,78 @@ \caption{tree を stack して目的の node まで辿った例} \label{fig:rbt-stack} \end{figure} - + -このようにして Gears Agda にて Binary Tree を実装していく． +このようにして Gears Agda にて Binary Tree を実装していく。 \subsection{Gears Agda における Binary Tree の実装} -Binary Tree と 遷移させる Data Gear となる Env の定義は Code \ref{bt_env} のようになる． +Binary Tree と 遷移させる DataGear となる Env の定義は \coderef{bt_env} のようになる。 -\lstinputlisting[label=bt_env, caption=Binary Tree の Data Gear] {src/bt_impl/bt_env.agda.replaced} +\lstinputlisting[label=code:bt_env, caption=Binary Tree の DataGear] {src/bt_impl/bt_env.agda.replaced} -bt は，木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように -「A : Set n」となっている． -そして left, right には bt A を持つようにし，木構造を構築している． +bt は、木での順序としての意味を持つ key とその中身 value はどのような型でも入れられるように +「A : Set n」となっている。 +そして left, right には bt A を持つようにし、木構造を構築している。 -Env では， find, insert, delete の対象となる値を保存し， Code Gear に与えられるようにするために -varn, varv を持っている． -加えて変更を加える bt を持つ vart と，前述した木構造を持っておくための List である -varl を Env に設定している． +Env では、 find, insert, delete の対象となる値を保存し、 CodeGear に与えられるようにするために +varn, varv を持っている。 +加えて変更を加える bt を持つ vart と、前述した木構造を持っておくための List である +varl を Env に設定している。 -7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る Code Gear が -Code \ref{bt_find_impl} になる． +7章で述べた Gears Agda での木構造を保ったまま root から目的のnodeまで辿る CodeGear が +\coderef{bt_find_impl} になる。 -\lstinputlisting[label=bt_find_impl, caption=root から目的のnodeまで辿る Code Gear] {src/bt_impl/find.agda.replaced} +\lstinputlisting[label=code:bt_find_impl, caption=root から目的のnodeまで辿る CodeGear] {src/bt_impl/find.agda.replaced} -まず，関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している． -ここで展開しているのは Env の vart で，そのまま Env から展開した vart をパターンマッチすると -Agda が追えなくなってしまい，\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう． +まず、関数の実装が始まってすぐに Env の vartを指定したものと引数をそのまま find-c の関数に遷移している。 +ここで展開しているのは Env の vart で、そのまま Env から展開した vart をパターンマッチすると +Agda が追えなくなってしまい、\{-$\#$ TERMINATING $\#$-\} を使用することになってしまう。 -そのため関数を新たに定義し，展開したものを受け取り，パターンマッチすることで +そのため関数を新たに定義し、展開したものを受け取り、パターンマッチすることで \{-$\#$ TERMINATING $\#$-\} を使用せずに loopを定義できるようになる。 -木を stack に入れるのは単純で，操作の対象の key となる varn と -node のkeyを比較を行う． -その後、本来の木構造と同じで，操作の対象の key が小さいなら -left の tree を次の node として遷移する． -大きいなら right の tree を次の node として遷移していく． +木を stack に入れるのは単純で、操作の対象の key となる varn と +node のkeyを比較を行う。 +その後、本来の木構造と同じで、操作の対象の key が小さいなら +left の tree を次の node として遷移する。 +大きいなら right の tree を次の node として遷移していく。 -操作の対象となる node に辿り着き，操作を行った後， -Stack に持っている tree から再構築を行う． +操作の対象となる node に辿り着き、操作を行った後、 +Stack に持っている tree から再構築を行う。 -そのコードが Code \ref{bt_replace_impl} となる。 +そのコードが \coderef{bt_replace_impl} となる。 -\lstinputlisting[label=bt_replace_impl, caption=Stack から tree を再構築する Code Gear] {src/bt_impl/replace.agda.replaced} +\lstinputlisting[label=code:bt_replace_impl, caption=Stack から tree を再構築する CodeGear] {src/bt_impl/replace.agda.replaced} -これも Code \ref{bt_find_impl} と同じように構成されており， -varn と node の key を比較し，vart を List から持ってきた node の どこに加えるかを決めるようになっている． +これも \coderef{bt_find_impl} と同じように構成されており、 +varn と node の key を比較し、vart を List から持ってきた node の どこに加えるかを決めるようになっている。 -以上の流れを繋げることで，Binary Tree の insert と find を実装できた． -delete は insert の値を消すようにすると実装ができる． +以上の流れを繋げることで、Binary Tree の insert と find を実装できた。 +delete は insert の値を消すようにすると実装ができる。 \subsection{Gears Agda における Binary Tree の検証} -検証も前述した While Loop の 検証と同じようにしていく． -しかし， Binary Tree の不変条件は2つ以上あるため，これを関数定義の際に全て書くと -煩雑になってしまうため，事前に記述して関数化しておく． -それが Code \ref{bt_invariant} になる． +検証も前述した While Loop の 検証と同じようにしていく。 +しかし、 Binary Tree の Invariant は2つ以上あるため、これを関数定義の際に全て書くと +煩雑になってしまうため、事前に記述して関数化しておく。 +それが\coderef{bt_invariant}になる。 -\lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/invariant.agda.replaced} +\lstinputlisting[label=code:bt_invariant, caption=Binary Tree の Invariant] {src/bt_verif/invariant.agda.replaced} -この不変条件は，treeInvariant が tree の 左にある node の key が小さく， -右にある node の方が大きいことを条件としている． +この Invariant は、treeInvariant が tree の 左にある node の key が小さく、 +右にある node の方が大きいことを条件としている。 -stackInvariant は Stack にある tree が，次に取り出す Tree の一部であることを -条件としている． +stackInvariant は Stack にある tree が、次に取り出す Tree の一部であることを +条件としている。 -これを先ほど実装した Code Gear に対して加えることで検証していく． -先ほど実装した Code \ref{bt_find_impl} に対して加えると Code ref のようになる． +これを先ほど実装した CodeGear に対して加えることで検証していく。 +先ほど実装した \coderef{bt_find_impl} に対して加えると \coderef{bt_invariant} のようになる。 -\lstinputlisting[label=bt_invariant, caption=Binary Tree の 不変条件] {src/bt_verif/find.agda.replaced} +\lstinputlisting[label=code:bt_invariant, caption=Binary Tree の検証] {src/bt_verif/find.agda.replaced} 現時点では条件を満たしていることの証明まで行っていないが -コード中の {!!} に記述を行い，前述した While Loop と同じように中身を記述することで検証を行える． +コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。
--- a/Paper/tex/while_loop.tex Thu Feb 02 17:49:33 2023 +0900 +++ b/Paper/tex/while_loop.tex Thu Feb 02 20:52:51 2023 +0900 @@ -1,86 +1,86 @@ \section{Gears Agda にて Hoare Logic を用いた検証の例} -ここでは Gears Agda にて Hoare Logic を用いた検証の例として， - While Loop プログラムを実装・検証する． +ここでは Gears Agda にて Hoare Logic を用いた検証の例として、 + While Loop プログラムを実装・検証する。 %% ここかその前にinvariantの説明した方がよい？ \subsection{While Loop の実装} -まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する． -実装はまず， Code \ref{while-loop-dg} のように Code Gear に遷移させる Data Gear の定義から行う． -\lstinputlisting[label=while-loop-dg, caption=Data Gearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced} +まずは前述した Gears Agda の記述形式に基づいて While Loop を実装する。 +実装はまず、 \coderef{while-loop-dg} のように CodeGear に遷移させる DataGear の定義から行う。 +\lstinputlisting[label=code:while-loop-dg, caption=DataGearの定義] {src/while_loop_impl/while_loop_dg.agda.replaced} -そのため最初の Code Gear は引数を受け取り，Envを作成する Code Gear となる Code \ref{while_init_cg}． +そのため最初の CodeGear は引数を受け取り、Envを作成する CodeGear となる \coderef{while_init_cg}。 -\lstinputlisting[label=while_init_cg, caption=Data Gear の定義を行う Code Gear] {src/while_loop_impl/init_cg.agda.replaced} +\lstinputlisting[label=code:while_init_cg, caption=DataGear の定義を行う CodeGear] {src/while_loop_impl/init_cg.agda.replaced} -次に，目的である While Loop の実装を行う．ソースコードは Code \ref{while-loop} のようになる． +次に、目的である While Loop の実装を行う。ソースコードは coderef{while-loop} のようになる。 -\lstinputlisting[label=while-loop, caption=Loop の部分を担う Code Gears] {src/while_loop_impl/while_loop.agda.replaced} +\lstinputlisting[label=code:while-loop, caption=Loop の部分を担う CodeGears] {src/while_loop_impl/while_loop.agda.replaced} -また Agda では停止性の検出機能が存在し， -プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る． +また Agda では停止性の検出機能が存在し、 +プログラム中 に停止しない記述が存在するとコンパイル時にエラーが出る。 その場合は関数定義の直前に \{-$\#$ TERMINATING $\#$-\} のタグを付けると 停止しないプログラムをコンパイルすることができる -これらの Code Gear を繋げることで， While Loop を行う \coderef{while-loop} を実装することができる． +これらの CodeGear を繋げることで、 While Loop を行う \coderef{while-loop} を実装することができる。 -\lstinputlisting[label=code:while-loop, caption=While Loop を行う Code Gear] {src/while_loop_impl/while_loop_c.agda.replaced} +\lstinputlisting[label=code:while-loop, caption=While Loop を行う CodeGear] {src/while_loop_impl/while_loop_c.agda.replaced} \subsection{While Loop の検証} -While Loop の実装コードを元に，前述した Pre / Post Condition を記述していくことで -Hoare Logic を用いた検証を行う． +While Loop の実装コードを元に、前述した Pre / Post Condition を記述していくことで +Hoare Logic を用いた検証を行う。 -検証を行う Code Gear も Gears Agda による単純な実装と同じく Data Gear から行う．Code \ref{while_verif_init_cg} がそれに当たる． +検証を行う CodeGear も Gears Agda による単純な実装と同じく DataGear から行う。\coderef{while_verif_init_cg} がそれに当たる。 -\lstinputlisting[label=while_verif_init_cg, caption=While Loop を行う Code Gear] {src/while_loop_verif/init_cg.agda.replaced} +\lstinputlisting[label=code:while_verif_init_cg, caption=While Loop を行う CodeGear] {src/while_loop_verif/init_cg.agda.replaced} -今回は検証を行いたいため 5.1 で述べたように，実装に加えて Pre / Post Condition を持つ必要がある． -init時の Pre Condition のみ特殊で Agda での関数定義の際に記述し， -「Data Gear に正しく初期値が設定される」という条件を使用する．これが +今回は検証を行いたいため 5.1 で述べたように、実装に加えて Pre / Post Condition を持つ必要がある。 +init時の Pre Condition のみ特殊で Agda での関数定義の際に記述し、 +「DataGear に正しく初期値が設定される」という Invariant を使用する。これが ((vari env) $\equiv$ 0) $\wedge$ ((varn env) $\equiv$ c10) -に当たる． -そしてinit時以外の，Pre Condition と Post Condition には実行開始から実行終了までの間で不変の条件を記述する． -今回は While Loop の不変条件として， +に当たる。 +そしてinit時以外の、Pre Condition と Post Condition には実行開始から実行終了までの間の Invariant を記述する。 +今回は While Loop の Invariant として、 $今回loopさせたい回数(c10) = 残りのloopする回数(vern) + 今回loopした回数(vari)$ -を設定した．これがinit時の Post Condition となる． +を設定した。これがinit時の Post Condition となる。 -また，init時の Pre Condition と同じ値で -Post Condition を設定しなければならない． -init時の Pre Condition を Post Condition に変換する Code \ref{conversion} を記載する． +また、init時の Pre Condition と同じ値で +Post Condition を設定しなければならない。 +init時の Pre Condition を Post Condition に変換する \coderef{conversion} を記載する。 -\lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced} +\lstinputlisting[label=code:conversion, caption=init時の Pre Condition を Post Condition に変換する CodeGear] {src/while_loop_verif/conversion.agda.replaced} -ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため， -停止するまでこの Pre / Post Condition を用いる． +ここで変換されて作成された Post Condition はプログラム実行中の Invariant となるため、 +停止するまでこの Pre / Post Condition を用いる。 -以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが， Wile Loop の Loop 部分の検証を行う Code Gear となる． +以下の \coderef{loop_verif_cg} は停止性の検証を行っていないが、 Wile Loop の Loop 部分の検証を行う CodeGear となる。 -\lstinputlisting[label=loop_verif_cg, caption=停止性以外の Loop の検証も行う Code Gear] {src/while_loop_verif/while_loop.agda.replaced} +\lstinputlisting[label=code:loop_verif_cg, caption=停止性以外の Loop の検証も行う CodeGear] {src/while_loop_verif/while_loop.agda.replaced} -Loop が停止することを示していないため，関数定義の直前に \{-\# TERMINATING \#-\} が記述されている． -こちらも Loop の実装以外に，Pre / Post Condition を満たしているか検証を行い，次の Code Gear に渡している． +Loop が停止することを示していないため、関数定義の直前に \{-\# TERMINATING \#-\} が記述されている。 +こちらも Loop の実装以外に、Pre / Post Condition を満たしているか検証を行い、次の CodeGear に渡している。 -ここまでで定義した Pre / Post Consition が付いている Code Gear を繋げることで， -停止性以外の While Loop の検証を行う Code Gear を実装できる． +ここまでで定義した Pre / Post Consition が付いている CodeGear を繋げることで、 +停止性以外の While Loop の検証を行う CodeGear を実装できる。 -\lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う Code Gear] {src/while_loop_verif/verif_term.agda.replaced} +\lstinputlisting[label=loop_verif_cg, caption=停止性以外の While Loop の検証を行う CodeGear] {src/while_loop_verif/verif_term.agda.replaced} -停止性の検証も行う While Loop の検証を行う Code Gear を実装する +停止性の検証も行う While Loop の検証を行う CodeGear を実装する -\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の Code Gear] {src/while_loop_verif/verif_loop.agda.replaced} +\lstinputlisting[label=loop_verif_cg, caption=停止性の検証も行う Loop 部分の CodeGear] {src/while_loop_verif/verif_loop.agda.replaced} -停止することを Agda が理解できるように記述する． -そのため引数に減少する変数 reduce を追加し， -loop するとデクリメントするように実装する． +停止することを Agda が理解できるように記述する。 +そのため引数に減少する変数 reduce を追加し、 +loop するとデクリメントするように実装する。 -loop には先ほど実装した loop の部分を担う Code Gear が次の関数遷移先を引数に受け取れるようにした -whileLoopSeg を使用する． +loop には先ほど実装した loop の部分を担う CodeGear が次の関数遷移先を引数に受け取れるようにした +whileLoopSeg を使用する。 -そしてこれらを繋げて While Loop の検証を行える\coderef{loop_verif_cg} を実装できた． +そしてこれらを繋げて While Loop の検証を行える\coderef{loop_verif_cg} を実装できた。 -\lstinputlisting[label=code:loop_verif_cg, caption=停止性の検証も行う While Loop の Code Gear] {src/while_loop_verif/verif.agda.replaced} +\lstinputlisting[label=code:loop_verif_cg, caption=停止性の検証も行う While Loop の CodeGear] {src/while_loop_verif/verif.agda.replaced}