|
22
|
1 \relax
|
|
|
2 \providecommand\hyper@newdestlabel[2]{}
|
|
|
3 \providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
|
|
|
4 \HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
|
|
|
5 \global\let\oldcontentsline\contentsline
|
|
|
6 \gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
|
|
|
7 \global\let\oldnewlabel\newlabel
|
|
|
8 \gdef\newlabel#1#2{\newlabelxx{#1}#2}
|
|
|
9 \gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
|
|
|
10 \AtEndDocument{\ifx\hyper@anchor\@undefined
|
|
|
11 \let\contentsline\oldcontentsline
|
|
|
12 \let\newlabel\oldnewlabel
|
|
|
13 \fi}
|
|
|
14 \fi}
|
|
|
15 \global\let\hyper@last\relax
|
|
|
16 \gdef\HyperFirstAtBeginDocument#1{#1}
|
|
|
17 \providecommand*\HyPL@Entry[1]{}
|
|
32
|
18 \HyPL@Entry{0<</S/D>>}
|
|
|
19 \HyPL@Entry{1<</P()>>}
|
|
|
20 \HyPL@Entry{2<</S/r>>}
|
|
22
|
21 \@writefile{toc}{\contentsline {chapter}{研究関連論文業績}{iv}{chapter*.3}\protected@file@percent }
|
|
32
|
22 \HyPL@Entry{6<</S/D>>}
|
|
22
|
23 \citation{cbc-gcc}
|
|
|
24 \citation{agda}
|
|
|
25 \citation{ryokka-sigos}
|
|
|
26 \citation{EdmundM}
|
|
|
27 \citation{ikkun-master}
|
|
|
28 \@writefile{toc}{\contentsline {chapter}{\numberline {第1章}Gears Agda でのプログラムの検証}{6}{chapter.1}\protected@file@percent }
|
|
|
29 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
30 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
31 \citation{kaito-lola}
|
|
|
32 \@writefile{toc}{\contentsline {chapter}{\numberline {第2章}Continuation based C}{7}{chapter.2}\protected@file@percent }
|
|
|
33 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
34 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
35 \@writefile{toc}{\contentsline {section}{\numberline {2.1}CodeGear / DataGear}{7}{section.2.1}\protected@file@percent }
|
|
|
36 \@writefile{toc}{\contentsline {section}{\numberline {2.2}CbC と C言語の違い}{7}{section.2.2}\protected@file@percent }
|
|
|
37 \newlabel{code:fib_c}{{2.1}{7}{C言語で記述した フィボナッチ数列の n 番目を求めるコード}{lstlisting.2.1}{}}
|
|
|
38 \@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}C言語で記述した フィボナッチ数列の n 番目を求めるコード}{7}{lstlisting.2.1}\protected@file@percent }
|
|
|
39 \newlabel{code:fib_cbc}{{2.2}{8}{CbCで記述した フィボナッチ数列の n 番目を求めるコード}{lstlisting.2.2}{}}
|
|
|
40 \@writefile{lol}{\contentsline {lstlisting}{\numberline {2.2}CbCで記述した フィボナッチ数列の n 番目を求めるコード}{8}{lstlisting.2.2}\protected@file@percent }
|
|
|
41 \newlabel{code:c-ass}{{2.3}{8}{cで記述した際の fib 関数のアセンブラ}{lstlisting.2.3}{}}
|
|
|
42 \@writefile{lol}{\contentsline {lstlisting}{\numberline {2.3}cで記述した際の fib 関数のアセンブラ}{8}{lstlisting.2.3}\protected@file@percent }
|
|
|
43 \newlabel{code:cbc-ass}{{2.4}{9}{cbcで記述した際の fib 関数のアセンブラ}{lstlisting.2.4}{}}
|
|
|
44 \@writefile{lol}{\contentsline {lstlisting}{\numberline {2.4}cbcで記述した際の fib 関数のアセンブラ}{9}{lstlisting.2.4}\protected@file@percent }
|
|
|
45 \@writefile{toc}{\contentsline {section}{\numberline {2.3}Meta CodeGear / Meta DataGear}{10}{section.2.3}\protected@file@percent }
|
|
|
46 \@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces メタ計算を可視化した CodeGear と DataGear}}{10}{figure.2.1}\protected@file@percent }
|
|
|
47 \newlabel{fig:meta-cgdg}{{2.1}{10}{メタ計算を可視化した CodeGear と DataGear}{figure.2.1}{}}
|
|
|
48 \citation{agda-wiki}
|
|
|
49 \citation{Stump:2016:VFP:2841316}
|
|
|
50 \citation{agda-stdlib}
|
|
|
51 \@writefile{toc}{\contentsline {chapter}{\numberline {第3章}定理証明支援系言語 Agda}{11}{chapter.3}\protected@file@percent }
|
|
|
52 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
53 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
54 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Agdaの基本}{11}{section.3.1}\protected@file@percent }
|
|
|
55 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1.1}関数の実装}{11}{subsection.3.1.1}\protected@file@percent }
|
|
|
56 \newlabel{code:plus}{{3.1}{11}{plusの実装}{lstlisting.3.1}{}}
|
|
|
57 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.1}plusの実装}{11}{lstlisting.3.1}\protected@file@percent }
|
|
|
58 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1.2}二項演算子の実装}{12}{subsection.3.1.2}\protected@file@percent }
|
|
|
59 \newlabel{code:plus2}{{3.2}{12}{二項演算子を用いたplusの実装}{lstlisting.3.2}{}}
|
|
|
60 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.2}二項演算子を用いたplusの実装}{12}{lstlisting.3.2}\protected@file@percent }
|
|
|
61 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1.3}Data 型の実装}{12}{subsection.3.1.3}\protected@file@percent }
|
|
|
62 \newlabel{code:Nat}{{3.3}{12}{Natural の定義}{lstlisting.3.3}{}}
|
|
|
63 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.3}Natural の定義}{12}{lstlisting.3.3}\protected@file@percent }
|
|
|
64 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1.4}Record 型の実装}{13}{subsection.3.1.4}\protected@file@percent }
|
|
|
65 \newlabel{code:Andの定義}{{3.4}{13}{Andの記述}{lstlisting.3.4}{}}
|
|
|
66 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.4}Andの記述}{13}{lstlisting.3.4}\protected@file@percent }
|
|
|
67 \newlabel{code:syllogism}{{3.5}{13}{syllogism の記述}{lstlisting.3.5}{}}
|
|
|
68 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.5}syllogism の記述}{13}{lstlisting.3.5}\protected@file@percent }
|
|
|
69 \@writefile{toc}{\contentsline {section}{\numberline {3.2}本論で使用する Agda の記法}{13}{section.3.2}\protected@file@percent }
|
|
|
70 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2.1}Agdaの省略記法}{13}{subsection.3.2.1}\protected@file@percent }
|
|
|
71 \newlabel{code:abridgement}{{3.6}{14}{入力を省略する Agda コードの例}{lstlisting.3.6}{}}
|
|
|
72 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.6}入力を省略する Agda コードの例}{14}{lstlisting.3.6}\protected@file@percent }
|
|
|
73 \@writefile{toc}{\contentsline {section}{\numberline {3.3}Agdaによる定理証明}{14}{section.3.3}\protected@file@percent }
|
|
|
74 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3.1}自然数に0を足しても値が等しいことを証明するAgda}{14}{subsection.3.3.1}\protected@file@percent }
|
|
|
75 \newlabel{code:proof}{{3.7}{14}{自然数に0を足しても値が等しいことを証明するAgda}{lstlisting.3.7}{}}
|
|
|
76 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.7}自然数に0を足しても値が等しいことを証明するAgda}{14}{lstlisting.3.7}\protected@file@percent }
|
|
|
77 \newlabel{code:cong}{{3.8}{15}{congの定義}{lstlisting.3.8}{}}
|
|
|
78 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.8}congの定義}{15}{lstlisting.3.8}\protected@file@percent }
|
|
|
79 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3.2}加算の交換法則を証明するAgda}{15}{subsection.3.3.2}\protected@file@percent }
|
|
|
80 \newlabel{code:agda-term-post}{{3.9}{15}{加算の交換法則を証明するAgda}{lstlisting.3.9}{}}
|
|
|
81 \@writefile{lol}{\contentsline {lstlisting}{\numberline {3.9}加算の交換法則を証明するAgda}{15}{lstlisting.3.9}\protected@file@percent }
|
|
|
82 \@writefile{toc}{\contentsline {chapter}{\numberline {第4章}GearsAgda 形式で書く Agda}{17}{chapter.4}\protected@file@percent }
|
|
|
83 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
84 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
85 \newlabel{code:agda-dg}{{4.1}{17}{Agdaでの DataGear の定義}{lstlisting.4.1}{}}
|
|
|
86 \@writefile{lol}{\contentsline {lstlisting}{\numberline {4.1}Agdaでの DataGear の定義}{17}{lstlisting.4.1}\protected@file@percent }
|
|
|
87 \newlabel{code:agda-cg}{{4.2}{17}{Agdaでの CodeGear の定義}{lstlisting.4.2}{}}
|
|
|
88 \@writefile{lol}{\contentsline {lstlisting}{\numberline {4.2}Agdaでの CodeGear の定義}{17}{lstlisting.4.2}\protected@file@percent }
|
|
|
89 \citation{atton-master}
|
|
|
90 \newlabel{code:agda-not-cg}{{4.3}{18}{Agdaでの 停止性が示せない CodeGear の例}{lstlisting.4.3}{}}
|
|
|
91 \@writefile{lol}{\contentsline {lstlisting}{\numberline {4.3}Agdaでの 停止性が示せない CodeGear の例}{18}{lstlisting.4.3}\protected@file@percent }
|
|
|
92 \newlabel{code:agda-exec-cg}{{4.4}{18}{Agdaでの CodeGear の初期化}{lstlisting.4.4}{}}
|
|
|
93 \@writefile{lol}{\contentsline {lstlisting}{\numberline {4.4}Agdaでの CodeGear の初期化}{18}{lstlisting.4.4}\protected@file@percent }
|
|
|
94 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Gears Agda での Meta Gears}{18}{section.4.1}\protected@file@percent }
|
|
|
95 \citation{ryokka-sigos}
|
|
|
96 \citation{agda2-hoare}
|
|
|
97 \citation{cr-ryukyu}
|
|
|
98 \citation{hoare}
|
|
|
99 \@writefile{toc}{\contentsline {chapter}{\numberline {第5章}Gears Agda による定理証明}{20}{chapter.5}\protected@file@percent }
|
|
|
100 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
101 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
102 \@writefile{toc}{\contentsline {section}{\numberline {5.1}Hoare Logic}{20}{section.5.1}\protected@file@percent }
|
|
|
103 \@writefile{toc}{\contentsline {section}{\numberline {5.2}Invariant を用いた Hoare Logic による検証の方法 }{20}{section.5.2}\protected@file@percent }
|
|
|
104 \@writefile{toc}{\contentsline {section}{\numberline {5.3}Gears Agda にて Hoare Logic を用いた検証の例}{21}{section.5.3}\protected@file@percent }
|
|
|
105 \@writefile{toc}{\contentsline {subsection}{\numberline {5.3.1}While Loop の実装}{21}{subsection.5.3.1}\protected@file@percent }
|
|
|
106 \newlabel{code:while-loop-dg}{{5.1}{21}{DataGearの定義}{lstlisting.5.1}{}}
|
|
|
107 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.1}DataGearの定義}{21}{lstlisting.5.1}\protected@file@percent }
|
|
|
108 \newlabel{code:while_init_cg}{{5.2}{21}{DataGear の定義を行う CodeGear}{lstlisting.5.2}{}}
|
|
|
109 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.2}DataGear の定義を行う CodeGear}{21}{lstlisting.5.2}\protected@file@percent }
|
|
|
110 \newlabel{code:while-loop}{{5.3}{21}{Loop の部分を担う CodeGears}{lstlisting.5.3}{}}
|
|
|
111 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.3}Loop の部分を担う CodeGears}{21}{lstlisting.5.3}\protected@file@percent }
|
|
|
112 \newlabel{code:while-loop2}{{5.4}{22}{While Loop を行う CodeGear}{lstlisting.5.4}{}}
|
|
|
113 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.4}While Loop を行う CodeGear}{22}{lstlisting.5.4}\protected@file@percent }
|
|
|
114 \@writefile{toc}{\contentsline {subsection}{\numberline {5.3.2}While Loop の検証}{22}{subsection.5.3.2}\protected@file@percent }
|
|
|
115 \newlabel{code:while_verif_init_cg}{{5.5}{22}{While Loop を行う CodeGear}{lstlisting.5.5}{}}
|
|
|
116 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.5}While Loop を行う CodeGear}{22}{lstlisting.5.5}\protected@file@percent }
|
|
|
117 \newlabel{code:conversion}{{5.6}{22}{init時の Pre Condition を Post Condition に変換する CodeGear}{lstlisting.5.6}{}}
|
|
|
118 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.6}init時の Pre Condition を Post Condition に変換する CodeGear}{22}{lstlisting.5.6}\protected@file@percent }
|
|
|
119 \newlabel{code:loop_verif_cg1}{{5.7}{23}{停止性以外の Loop の検証も行う CodeGear}{lstlisting.5.7}{}}
|
|
|
120 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.7}停止性以外の Loop の検証も行う CodeGear}{23}{lstlisting.5.7}\protected@file@percent }
|
|
|
121 \newlabel{code:loop_verif_cg2}{{5.8}{23}{停止性以外の While Loop の検証を行う CodeGear}{lstlisting.5.8}{}}
|
|
|
122 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.8}停止性以外の While Loop の検証を行う CodeGear}{23}{lstlisting.5.8}\protected@file@percent }
|
|
|
123 \citation{rbtree}
|
|
|
124 \newlabel{code:loop_verif_cg3}{{5.9}{24}{停止性の検証も行う Loop 部分の CodeGear}{lstlisting.5.9}{}}
|
|
|
125 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.9}停止性の検証も行う Loop 部分の CodeGear}{24}{lstlisting.5.9}\protected@file@percent }
|
|
|
126 \newlabel{code:loop_verif_cg4}{{5.10}{24}{停止性の検証も行う While Loop の CodeGear}{lstlisting.5.10}{}}
|
|
|
127 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.10}停止性の検証も行う While Loop の CodeGear}{24}{lstlisting.5.10}\protected@file@percent }
|
|
|
128 \@writefile{toc}{\contentsline {section}{\numberline {5.4}Gears Agda における Binary Tree の検証}{24}{section.5.4}\protected@file@percent }
|
|
|
129 \@writefile{toc}{\contentsline {subsection}{\numberline {5.4.1}Gears Agda における木構造の設計}{24}{subsection.5.4.1}\protected@file@percent }
|
|
|
130 \@writefile{lof}{\contentsline {figure}{\numberline {5.1}{\ignorespaces tree を stack して目的の node まで辿った例}}{25}{figure.5.1}\protected@file@percent }
|
|
|
131 \newlabel{fig:rbt-stack}{{5.1}{25}{tree を stack して目的の node まで辿った例}{figure.5.1}{}}
|
|
|
132 \@writefile{toc}{\contentsline {subsection}{\numberline {5.4.2}Gears Agda における Binary Tree の実装}{25}{subsection.5.4.2}\protected@file@percent }
|
|
|
133 \newlabel{code:bt_env}{{5.11}{25}{Binary Tree の DataGear}{lstlisting.5.11}{}}
|
|
|
134 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.11}Binary Tree の DataGear}{25}{lstlisting.5.11}\protected@file@percent }
|
|
|
135 \newlabel{code:bt_find_impl}{{5.12}{26}{root から目的のnodeまで辿る CodeGear}{lstlisting.5.12}{}}
|
|
|
136 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.12}root から目的のnodeまで辿る CodeGear}{26}{lstlisting.5.12}\protected@file@percent }
|
|
|
137 \newlabel{code:bt_replace_impl}{{5.13}{26}{Stack から tree を再構築する CodeGear}{lstlisting.5.13}{}}
|
|
|
138 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.13}Stack から tree を再構築する CodeGear}{26}{lstlisting.5.13}\protected@file@percent }
|
|
|
139 \@writefile{toc}{\contentsline {subsection}{\numberline {5.4.3}Gears Agda における Binary Tree の検証}{27}{subsection.5.4.3}\protected@file@percent }
|
|
|
140 \newlabel{code:bt_invariant}{{5.14}{27}{Binary Tree の Invariant}{lstlisting.5.14}{}}
|
|
|
141 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.14}Binary Tree の Invariant}{27}{lstlisting.5.14}\protected@file@percent }
|
|
|
142 \newlabel{code:bt_invariant2}{{5.15}{28}{Binary Tree の検証}{lstlisting.5.15}{}}
|
|
|
143 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.15}Binary Tree の検証}{28}{lstlisting.5.15}\protected@file@percent }
|
|
|
144 \citation{parusu-master}
|
|
|
145 \@writefile{toc}{\contentsline {chapter}{\numberline {第6章}Gears Agda によるモデル検査}{29}{chapter.6}\protected@file@percent }
|
|
|
146 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
147 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
148 \@writefile{toc}{\contentsline {section}{\numberline {6.1}モデル検査とは}{29}{section.6.1}\protected@file@percent }
|
|
|
149 \@writefile{toc}{\contentsline {section}{\numberline {6.2}Dining Philosophers Problem}{29}{section.6.2}\protected@file@percent }
|
|
|
150 \citation{spin}
|
|
|
151 \@writefile{lof}{\contentsline {figure}{\numberline {6.1}{\ignorespaces Dining Philosophers Program のイメージ図}}{30}{figure.6.1}\protected@file@percent }
|
|
|
152 \newlabel{fig:DPP}{{6.1}{30}{Dining Philosophers Program のイメージ図}{figure.6.1}{}}
|
|
|
153 \@writefile{toc}{\contentsline {section}{\numberline {6.3}SPINによるモデル検査}{30}{section.6.3}\protected@file@percent }
|
|
|
154 \newlabel{code:spin-dpp}{{6.1}{30}{SPINにてDPPをモデル検査する際のコードの一部}{lstlisting.6.1}{}}
|
|
|
155 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.1}SPINにてDPPをモデル検査する際のコードの一部}{30}{lstlisting.6.1}\protected@file@percent }
|
|
|
156 \@writefile{toc}{\contentsline {section}{\numberline {6.4}Gears Agdaによるモデル検査の流れ}{31}{section.6.4}\protected@file@percent }
|
|
|
157 \@writefile{lof}{\contentsline {figure}{\numberline {6.2}{\ignorespaces SPINにて作成した状態遷移図}}{32}{figure.6.2}\protected@file@percent }
|
|
|
158 \newlabel{fig:DPP-model}{{6.2}{32}{SPINにて作成した状態遷移図}{figure.6.2}{}}
|
|
|
159 \@writefile{toc}{\contentsline {section}{\numberline {6.5}Gears Agda によるDPPの実装}{33}{section.6.5}\protected@file@percent }
|
|
|
160 \newlabel{code:agda-dpp-state}{{6.2}{33}{Gears Agdaでの DPP の 哲学者の状態}{lstlisting.6.2}{}}
|
|
|
161 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.2}Gears Agdaでの DPP の 哲学者の状態}{33}{lstlisting.6.2}\protected@file@percent }
|
|
|
162 \newlabel{code:agda-dpp-process}{{6.3}{33}{Gears Agdaでの DPP の プロセス}{lstlisting.6.3}{}}
|
|
|
163 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.3}Gears Agdaでの DPP の プロセス}{33}{lstlisting.6.3}\protected@file@percent }
|
|
|
164 \newlabel{code:agda-dpp-dg}{{6.4}{33}{Gears Agdaでの DPP の DataGear}{lstlisting.6.4}{}}
|
|
|
165 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.4}Gears Agdaでの DPP の DataGear}{33}{lstlisting.6.4}\protected@file@percent }
|
|
|
166 \newlabel{code:agda-dpp-init}{{6.5}{34}{Gears Agdaでの DPP の DataGear のinit}{lstlisting.6.5}{}}
|
|
|
167 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.5}Gears Agdaでの DPP の DataGear のinit}{34}{lstlisting.6.5}\protected@file@percent }
|
|
|
168 \newlabel{agda-dpp-step}{{6.6}{34}{Gears Agdaでの DPP の step 実行}{lstlisting.6.6}{}}
|
|
|
169 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.6}Gears Agdaでの DPP の step 実行}{34}{lstlisting.6.6}\protected@file@percent }
|
|
|
170 \newlabel{code:agda-dpp-lfork}{{6.7}{34}{Gears Agdaでの DPP の左のフォークを取る記述}{lstlisting.6.7}{}}
|
|
|
171 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.7}Gears Agdaでの DPP の左のフォークを取る記述}{34}{lstlisting.6.7}\protected@file@percent }
|
|
|
172 \@writefile{toc}{\contentsline {section}{\numberline {6.6}Gears Agda によるDPPの検証}{35}{section.6.6}\protected@file@percent }
|
|
|
173 \newlabel{code:dpp-mdg}{{6.8}{35}{Gears Agda で DPP のモデル検査を行うための Meta DataGear}{lstlisting.6.8}{}}
|
|
|
174 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.8}Gears Agda で DPP のモデル検査を行うための Meta DataGear}{35}{lstlisting.6.8}\protected@file@percent }
|
|
|
175 \newlabel{code:dpp-mcg-branch}{{6.9}{36}{状態の分岐数をカウントする Meta DataGear の定義}{lstlisting.6.9}{}}
|
|
|
176 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.9}状態の分岐数をカウントする Meta DataGear の定義}{36}{lstlisting.6.9}\protected@file@percent }
|
|
|
177 \newlabel{code:dpp-judge-mcg}{{6.10}{37}{DPP での dead lock を検知する Meta CodeGear}{lstlisting.6.10}{}}
|
|
|
178 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.10}DPP での dead lock を検知する Meta CodeGear}{37}{lstlisting.6.10}\protected@file@percent }
|
|
|
179 \newlabel{code:dpp-exclude-state-mcg}{{6.11}{38}{重複しているstateを除外する Meta CodeGear}{lstlisting.6.11}{}}
|
|
|
180 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6.11}重複しているstateを除外する Meta CodeGear}{38}{lstlisting.6.11}\protected@file@percent }
|
|
|
181 \@writefile{toc}{\contentsline {section}{\numberline {6.7}Gears Agda による live lockの検証方法について}{39}{section.6.7}\protected@file@percent }
|
|
|
182 \@writefile{toc}{\contentsline {section}{\numberline {6.8}Gears Agda でのモデル検査の評価}{39}{section.6.8}\protected@file@percent }
|
|
|
183 \citation{mitsuki-prosym}
|
|
|
184 \citation{model}
|
|
|
185 \@writefile{toc}{\contentsline {chapter}{\numberline {第7章}まとめと今後の展望}{41}{chapter.7}\protected@file@percent }
|
|
|
186 \@writefile{lof}{\addvspace {10\p@ }}
|
|
|
187 \@writefile{lot}{\addvspace {10\p@ }}
|
|
|
188 \@writefile{toc}{\contentsline {section}{\numberline {7.1}今後の課題}{41}{section.7.1}\protected@file@percent }
|
|
|
189 \citation{*}
|
|
|
190 \bibdata{reference}
|
|
|
191 \@writefile{toc}{\contentsline {chapter}{謝辞}{42}{chapter*.7}\protected@file@percent }
|
|
|
192 \bibcite{cbc-gcc}{1}
|
|
|
193 \bibcite{agda}{2}
|
|
|
194 \bibcite{ryokka-sigos}{3}
|
|
|
195 \bibcite{EdmundM}{4}
|
|
|
196 \bibcite{ikkun-master}{5}
|
|
|
197 \bibcite{kaito-lola}{6}
|
|
|
198 \bibcite{agda-wiki}{7}
|
|
|
199 \bibcite{Stump:2016:VFP:2841316}{8}
|
|
|
200 \bibcite{agda-stdlib}{9}
|
|
|
201 \bibcite{atton-master}{10}
|
|
|
202 \bibcite{agda2-hoare}{11}
|
|
|
203 \bibcite{cr-ryukyu}{12}
|
|
|
204 \bibcite{hoare}{13}
|
|
|
205 \@writefile{toc}{\contentsline {chapter}{参考文献}{43}{chapter*.8}\protected@file@percent }
|
|
|
206 \bibcite{rbtree}{14}
|
|
|
207 \bibcite{parusu-master}{15}
|
|
|
208 \bibcite{spin}{16}
|
|
|
209 \bibcite{mitsuki-prosym}{17}
|
|
|
210 \bibcite{model}{18}
|
|
|
211 \bibstyle{junsrt}
|
|
32
|
212 \gdef \@abspage@last{50}
|
