\contentsline {chapter}{研究関連論文業績}{iv}{chapter*.3}%
\contentsline {chapter}{\numberline {第1章}Gears Agda でのプログラムの検証}{6}{chapter.1}%
\contentsline {chapter}{\numberline {第2章}Continuation based C}{7}{chapter.2}%
\contentsline {section}{\numberline {2.1}CodeGear / DataGear}{7}{section.2.1}%
\contentsline {section}{\numberline {2.2}CbC と C言語の違い}{7}{section.2.2}%
\contentsline {section}{\numberline {2.3}Meta CodeGear / Meta DataGear}{10}{section.2.3}%
\contentsline {chapter}{\numberline {第3章}定理証明支援系言語 Agda}{11}{chapter.3}%
\contentsline {section}{\numberline {3.1}Agdaの基本}{11}{section.3.1}%
\contentsline {subsection}{\numberline {3.1.1}関数の実装}{11}{subsection.3.1.1}%
\contentsline {subsection}{\numberline {3.1.2}二項演算子の実装}{12}{subsection.3.1.2}%
\contentsline {subsection}{\numberline {3.1.3}Data 型の実装}{12}{subsection.3.1.3}%
\contentsline {subsection}{\numberline {3.1.4}Record 型の実装}{13}{subsection.3.1.4}%
\contentsline {section}{\numberline {3.2}本論で使用する Agda の記法}{13}{section.3.2}%
\contentsline {subsection}{\numberline {3.2.1}Agdaの省略記法}{13}{subsection.3.2.1}%
\contentsline {section}{\numberline {3.3}Agdaによる定理証明}{14}{section.3.3}%
\contentsline {subsection}{\numberline {3.3.1}自然数に0を足しても値が等しいことを証明するAgda}{14}{subsection.3.3.1}%
\contentsline {subsection}{\numberline {3.3.2}加算の交換法則を証明するAgda}{15}{subsection.3.3.2}%
\contentsline {chapter}{\numberline {第4章}GearsAgda 形式で書く Agda}{17}{chapter.4}%
\contentsline {section}{\numberline {4.1}Gears Agda での Meta Gears}{18}{section.4.1}%
\contentsline {chapter}{\numberline {第5章}Gears Agda による定理証明}{20}{chapter.5}%
\contentsline {section}{\numberline {5.1}Hoare Logic}{20}{section.5.1}%
\contentsline {section}{\numberline {5.2}Invariant を用いた Hoare Logic による検証の方法 }{20}{section.5.2}%
\contentsline {section}{\numberline {5.3}Gears Agda にて Hoare Logic を用いた検証の例}{21}{section.5.3}%
\contentsline {subsection}{\numberline {5.3.1}While Loop の実装}{21}{subsection.5.3.1}%
\contentsline {subsection}{\numberline {5.3.2}While Loop の検証}{22}{subsection.5.3.2}%
\contentsline {section}{\numberline {5.4}Gears Agda における Binary Tree の検証}{24}{section.5.4}%
\contentsline {subsection}{\numberline {5.4.1}Gears Agda における木構造の設計}{24}{subsection.5.4.1}%
\contentsline {subsection}{\numberline {5.4.2}Gears Agda における Binary Tree の実装}{25}{subsection.5.4.2}%
\contentsline {subsection}{\numberline {5.4.3}Gears Agda における Binary Tree の検証}{27}{subsection.5.4.3}%
\contentsline {chapter}{\numberline {第6章}Gears Agda によるモデル検査}{29}{chapter.6}%
\contentsline {section}{\numberline {6.1}モデル検査とは}{29}{section.6.1}%
\contentsline {section}{\numberline {6.2}Dining Philosophers Problem}{29}{section.6.2}%
\contentsline {section}{\numberline {6.3}SPINによるモデル検査}{30}{section.6.3}%
\contentsline {section}{\numberline {6.4}Gears Agdaによるモデル検査の流れ}{31}{section.6.4}%
\contentsline {section}{\numberline {6.5}Gears Agda によるDPPの実装}{33}{section.6.5}%
\contentsline {section}{\numberline {6.6}Gears Agda によるDPPの検証}{35}{section.6.6}%
\contentsline {section}{\numberline {6.7}Gears Agda による live lockの検証方法について}{39}{section.6.7}%
\contentsline {section}{\numberline {6.8}Gears Agda でのモデル検査の評価}{39}{section.6.8}%
\contentsline {chapter}{\numberline {第7章}まとめと今後の展望}{41}{chapter.7}%
\contentsline {section}{\numberline {7.1}今後の課題}{41}{section.7.1}%
\contentsline {chapter}{謝辞}{42}{chapter*.7}%
\contentsline {chapter}{参考文献}{43}{chapter*.8}%