\relax 
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand*\HyPL@Entry[1]{}
\HyPL@Entry{0<</S/D>>}
\HyPL@Entry{1<</P()>>}
\HyPL@Entry{2<</S/r>>}
\@writefile{toc}{\contentsline {chapter}{研究関連論文業績}{iv}{chapter*.3}\protected@file@percent }
\HyPL@Entry{6<</S/D>>}
\citation{cbc-gcc}
\citation{agda}
\citation{ryokka-sigos}
\citation{EdmundM}
\citation{ikkun-master}
\@writefile{toc}{\contentsline {chapter}{\numberline {第1章}Gears Agda でのプログラムの検証}{6}{chapter.1}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\citation{kaito-lola}
\@writefile{toc}{\contentsline {chapter}{\numberline {第2章}Continuation based C}{7}{chapter.2}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {2.1}CodeGear / DataGear}{7}{section.2.1}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {2.2}CbC と C言語の違い}{7}{section.2.2}\protected@file@percent }
\newlabel{code:fib_c}{{2.1}{7}{C言語で記述した フィボナッチ数列の n 番目を求めるコード}{lstlisting.2.1}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}C言語で記述した フィボナッチ数列の n 番目を求めるコード}{7}{lstlisting.2.1}\protected@file@percent }
\newlabel{code:fib_cbc}{{2.2}{8}{CbCで記述した フィボナッチ数列の n 番目を求めるコード}{lstlisting.2.2}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.2}CbCで記述した フィボナッチ数列の n 番目を求めるコード}{8}{lstlisting.2.2}\protected@file@percent }
\newlabel{code:c-ass}{{2.3}{8}{cで記述した際の fib 関数のアセンブラ}{lstlisting.2.3}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.3}cで記述した際の fib 関数のアセンブラ}{8}{lstlisting.2.3}\protected@file@percent }
\newlabel{code:cbc-ass}{{2.4}{9}{cbcで記述した際の fib 関数のアセンブラ}{lstlisting.2.4}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.4}cbcで記述した際の fib 関数のアセンブラ}{9}{lstlisting.2.4}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {2.3}Meta CodeGear / Meta DataGear}{10}{section.2.3}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces メタ計算を可視化した CodeGear と DataGear}}{10}{figure.2.1}\protected@file@percent }
\newlabel{fig:meta-cgdg}{{2.1}{10}{メタ計算を可視化した CodeGear と DataGear}{figure.2.1}{}}
\citation{agda-wiki}
\citation{Stump:2016:VFP:2841316}
\citation{agda-stdlib}
\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}定理証明支援系言語 Agda}{11}{chapter.3}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {3.1}Agdaの基本}{11}{section.3.1}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.1}関数の実装}{11}{subsection.3.1.1}\protected@file@percent }
\newlabel{code:plus}{{3.1}{11}{plusの実装}{lstlisting.3.1}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.1}plusの実装}{11}{lstlisting.3.1}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.2}二項演算子の実装}{12}{subsection.3.1.2}\protected@file@percent }
\newlabel{code:plus2}{{3.2}{12}{二項演算子を用いたplusの実装}{lstlisting.3.2}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.2}二項演算子を用いたplusの実装}{12}{lstlisting.3.2}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.3}Data 型の実装}{12}{subsection.3.1.3}\protected@file@percent }
\newlabel{code:Nat}{{3.3}{12}{Natural の定義}{lstlisting.3.3}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.3}Natural の定義}{12}{lstlisting.3.3}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.4}Record 型の実装}{13}{subsection.3.1.4}\protected@file@percent }
\newlabel{code:Andの定義}{{3.4}{13}{Andの記述}{lstlisting.3.4}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.4}Andの記述}{13}{lstlisting.3.4}\protected@file@percent }
\newlabel{code:syllogism}{{3.5}{13}{syllogism の記述}{lstlisting.3.5}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.5}syllogism の記述}{13}{lstlisting.3.5}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {3.2}本論で使用する Agda の記法}{13}{section.3.2}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Agdaの省略記法}{13}{subsection.3.2.1}\protected@file@percent }
\newlabel{code:abridgement}{{3.6}{14}{入力を省略する Agda コードの例}{lstlisting.3.6}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.6}入力を省略する Agda コードの例}{14}{lstlisting.3.6}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {3.3}Agdaによる定理証明}{14}{section.3.3}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.1}自然数に0を足しても値が等しいことを証明するAgda}{14}{subsection.3.3.1}\protected@file@percent }
\newlabel{code:proof}{{3.7}{14}{自然数に0を足しても値が等しいことを証明するAgda}{lstlisting.3.7}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.7}自然数に0を足しても値が等しいことを証明するAgda}{14}{lstlisting.3.7}\protected@file@percent }
\newlabel{code:cong}{{3.8}{15}{congの定義}{lstlisting.3.8}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.8}congの定義}{15}{lstlisting.3.8}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.2}加算の交換法則を証明するAgda}{15}{subsection.3.3.2}\protected@file@percent }
\newlabel{code:agda-term-post}{{3.9}{15}{加算の交換法則を証明するAgda}{lstlisting.3.9}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.9}加算の交換法則を証明するAgda}{15}{lstlisting.3.9}\protected@file@percent }
\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}GearsAgda 形式で書く Agda}{17}{chapter.4}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{code:agda-dg}{{4.1}{17}{Agdaでの DataGear の定義}{lstlisting.4.1}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.1}Agdaでの DataGear の定義}{17}{lstlisting.4.1}\protected@file@percent }
\newlabel{code:agda-cg}{{4.2}{17}{Agdaでの CodeGear の定義}{lstlisting.4.2}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.2}Agdaでの CodeGear の定義}{17}{lstlisting.4.2}\protected@file@percent }
\citation{atton-master}
\newlabel{code:agda-not-cg}{{4.3}{18}{Agdaでの 停止性が示せない CodeGear の例}{lstlisting.4.3}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.3}Agdaでの 停止性が示せない CodeGear の例}{18}{lstlisting.4.3}\protected@file@percent }
\newlabel{code:agda-exec-cg}{{4.4}{18}{Agdaでの CodeGear の初期化}{lstlisting.4.4}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4.4}Agdaでの CodeGear の初期化}{18}{lstlisting.4.4}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4.1}Gears Agda での Meta Gears}{18}{section.4.1}\protected@file@percent }
\citation{ryokka-sigos}
\citation{agda2-hoare}
\citation{cr-ryukyu}
\citation{hoare}
\@writefile{toc}{\contentsline {chapter}{\numberline {第5章}Gears Agda による定理証明}{20}{chapter.5}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {5.1}Hoare Logic}{20}{section.5.1}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5.2}Invariant を用いた Hoare Logic による検証の方法 }{20}{section.5.2}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5.3}Gears Agda にて Hoare Logic を用いた検証の例}{21}{section.5.3}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.1}While Loop の実装}{21}{subsection.5.3.1}\protected@file@percent }
\newlabel{code:while-loop-dg}{{5.1}{21}{DataGearの定義}{lstlisting.5.1}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.1}DataGearの定義}{21}{lstlisting.5.1}\protected@file@percent }
\newlabel{code:while_init_cg}{{5.2}{21}{DataGear の定義を行う CodeGear}{lstlisting.5.2}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.2}DataGear の定義を行う CodeGear}{21}{lstlisting.5.2}\protected@file@percent }
\newlabel{code:while-loop}{{5.3}{21}{Loop の部分を担う CodeGears}{lstlisting.5.3}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.3}Loop の部分を担う CodeGears}{21}{lstlisting.5.3}\protected@file@percent }
\newlabel{code:while-loop2}{{5.4}{22}{While Loop を行う CodeGear}{lstlisting.5.4}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.4}While Loop を行う CodeGear}{22}{lstlisting.5.4}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.2}While Loop の検証}{22}{subsection.5.3.2}\protected@file@percent }
\newlabel{code:while_verif_init_cg}{{5.5}{22}{While Loop を行う CodeGear}{lstlisting.5.5}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.5}While Loop を行う CodeGear}{22}{lstlisting.5.5}\protected@file@percent }
\newlabel{code:conversion}{{5.6}{22}{init時の Pre Condition を Post Condition に変換する CodeGear}{lstlisting.5.6}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.6}init時の Pre Condition を Post Condition に変換する CodeGear}{22}{lstlisting.5.6}\protected@file@percent }
\newlabel{code:loop_verif_cg1}{{5.7}{23}{停止性以外の Loop の検証も行う CodeGear}{lstlisting.5.7}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.7}停止性以外の Loop の検証も行う CodeGear}{23}{lstlisting.5.7}\protected@file@percent }
\newlabel{code:loop_verif_cg2}{{5.8}{23}{停止性以外の While Loop の検証を行う CodeGear}{lstlisting.5.8}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.8}停止性以外の While Loop の検証を行う CodeGear}{23}{lstlisting.5.8}\protected@file@percent }
\citation{rbtree}
\newlabel{code:loop_verif_cg3}{{5.9}{24}{停止性の検証も行う Loop 部分の CodeGear}{lstlisting.5.9}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.9}停止性の検証も行う Loop 部分の CodeGear}{24}{lstlisting.5.9}\protected@file@percent }
\newlabel{code:loop_verif_cg4}{{5.10}{24}{停止性の検証も行う While Loop の CodeGear}{lstlisting.5.10}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.10}停止性の検証も行う While Loop の CodeGear}{24}{lstlisting.5.10}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5.4}Gears Agda における Binary Tree の検証}{24}{section.5.4}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.1}Gears Agda における木構造の設計}{24}{subsection.5.4.1}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {5.1}{\ignorespaces tree を stack して目的の node まで辿った例}}{25}{figure.5.1}\protected@file@percent }
\newlabel{fig:rbt-stack}{{5.1}{25}{tree を stack して目的の node まで辿った例}{figure.5.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.2}Gears Agda における Binary Tree の実装}{25}{subsection.5.4.2}\protected@file@percent }
\newlabel{code:bt_env}{{5.11}{25}{Binary Tree の DataGear}{lstlisting.5.11}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.11}Binary Tree の DataGear}{25}{lstlisting.5.11}\protected@file@percent }
\newlabel{code:bt_find_impl}{{5.12}{26}{root から目的のnodeまで辿る CodeGear}{lstlisting.5.12}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.12}root から目的のnodeまで辿る CodeGear}{26}{lstlisting.5.12}\protected@file@percent }
\newlabel{code:bt_replace_impl}{{5.13}{26}{Stack から tree を再構築する CodeGear}{lstlisting.5.13}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.13}Stack から tree を再構築する CodeGear}{26}{lstlisting.5.13}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4.3}Gears Agda における Binary Tree の検証}{27}{subsection.5.4.3}\protected@file@percent }
\newlabel{code:bt_invariant}{{5.14}{27}{Binary Tree の Invariant}{lstlisting.5.14}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.14}Binary Tree の Invariant}{27}{lstlisting.5.14}\protected@file@percent }
\newlabel{code:bt_invariant2}{{5.15}{28}{Binary Tree の検証}{lstlisting.5.15}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.15}Binary Tree の検証}{28}{lstlisting.5.15}\protected@file@percent }
\citation{parusu-master}
\@writefile{toc}{\contentsline {chapter}{\numberline {第6章}Gears Agda によるモデル検査}{29}{chapter.6}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {6.1}モデル検査とは}{29}{section.6.1}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6.2}Dining Philosophers Problem}{29}{section.6.2}\protected@file@percent }
\citation{spin}
\@writefile{lof}{\contentsline {figure}{\numberline {6.1}{\ignorespaces Dining Philosophers Program のイメージ図}}{30}{figure.6.1}\protected@file@percent }
\newlabel{fig:DPP}{{6.1}{30}{Dining Philosophers Program のイメージ図}{figure.6.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6.3}SPINによるモデル検査}{30}{section.6.3}\protected@file@percent }
\newlabel{code:spin-dpp}{{6.1}{30}{SPINにてDPPをモデル検査する際のコードの一部}{lstlisting.6.1}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.1}SPINにてDPPをモデル検査する際のコードの一部}{30}{lstlisting.6.1}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6.4}Gears Agdaによるモデル検査の流れ}{31}{section.6.4}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {6.2}{\ignorespaces SPINにて作成した状態遷移図}}{32}{figure.6.2}\protected@file@percent }
\newlabel{fig:DPP-model}{{6.2}{32}{SPINにて作成した状態遷移図}{figure.6.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6.5}Gears Agda によるDPPの実装}{33}{section.6.5}\protected@file@percent }
\newlabel{code:agda-dpp-state}{{6.2}{33}{Gears Agdaでの DPP の 哲学者の状態}{lstlisting.6.2}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.2}Gears Agdaでの DPP の 哲学者の状態}{33}{lstlisting.6.2}\protected@file@percent }
\newlabel{code:agda-dpp-process}{{6.3}{33}{Gears Agdaでの DPP の プロセス}{lstlisting.6.3}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.3}Gears Agdaでの DPP の プロセス}{33}{lstlisting.6.3}\protected@file@percent }
\newlabel{code:agda-dpp-dg}{{6.4}{33}{Gears Agdaでの DPP の DataGear}{lstlisting.6.4}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.4}Gears Agdaでの DPP の DataGear}{33}{lstlisting.6.4}\protected@file@percent }
\newlabel{code:agda-dpp-init}{{6.5}{34}{Gears Agdaでの DPP の DataGear のinit}{lstlisting.6.5}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.5}Gears Agdaでの DPP の DataGear のinit}{34}{lstlisting.6.5}\protected@file@percent }
\newlabel{agda-dpp-step}{{6.6}{34}{Gears Agdaでの DPP の step 実行}{lstlisting.6.6}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.6}Gears Agdaでの DPP の step 実行}{34}{lstlisting.6.6}\protected@file@percent }
\newlabel{code:agda-dpp-lfork}{{6.7}{34}{Gears Agdaでの DPP の左のフォークを取る記述}{lstlisting.6.7}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.7}Gears Agdaでの DPP の左のフォークを取る記述}{34}{lstlisting.6.7}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6.6}Gears Agda によるDPPの検証}{35}{section.6.6}\protected@file@percent }
\newlabel{code:dpp-mdg}{{6.8}{35}{Gears Agda で DPP のモデル検査を行うための Meta DataGear}{lstlisting.6.8}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.8}Gears Agda で DPP のモデル検査を行うための Meta DataGear}{35}{lstlisting.6.8}\protected@file@percent }
\newlabel{code:dpp-mcg-branch}{{6.9}{36}{状態の分岐数をカウントする Meta DataGear の定義}{lstlisting.6.9}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.9}状態の分岐数をカウントする Meta DataGear の定義}{36}{lstlisting.6.9}\protected@file@percent }
\newlabel{code:dpp-judge-mcg}{{6.10}{37}{DPP での dead lock を検知する Meta CodeGear}{lstlisting.6.10}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.10}DPP での dead lock を検知する Meta CodeGear}{37}{lstlisting.6.10}\protected@file@percent }
\newlabel{code:dpp-exclude-state-mcg}{{6.11}{38}{重複しているstateを除外する Meta CodeGear}{lstlisting.6.11}{}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6.11}重複しているstateを除外する Meta CodeGear}{38}{lstlisting.6.11}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6.7}Gears Agda による live lockの検証方法について}{39}{section.6.7}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6.8}Gears Agda でのモデル検査の評価}{39}{section.6.8}\protected@file@percent }
\citation{mitsuki-prosym}
\citation{model}
\@writefile{toc}{\contentsline {chapter}{\numberline {第7章}まとめと今後の展望}{41}{chapter.7}\protected@file@percent }
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {7.1}今後の課題}{41}{section.7.1}\protected@file@percent }
\citation{*}
\bibdata{reference}
\@writefile{toc}{\contentsline {chapter}{謝辞}{42}{chapter*.7}\protected@file@percent }
\bibcite{cbc-gcc}{1}
\bibcite{agda}{2}
\bibcite{ryokka-sigos}{3}
\bibcite{EdmundM}{4}
\bibcite{ikkun-master}{5}
\bibcite{kaito-lola}{6}
\bibcite{agda-wiki}{7}
\bibcite{Stump:2016:VFP:2841316}{8}
\bibcite{agda-stdlib}{9}
\bibcite{atton-master}{10}
\bibcite{agda2-hoare}{11}
\bibcite{cr-ryukyu}{12}
\bibcite{hoare}{13}
\@writefile{toc}{\contentsline {chapter}{参考文献}{43}{chapter*.8}\protected@file@percent }
\bibcite{rbtree}{14}
\bibcite{parusu-master}{15}
\bibcite{spin}{16}
\bibcite{mitsuki-prosym}{17}
\bibcite{model}{18}
\bibstyle{junsrt}
\gdef \@abspage@last{50}