Mercurial > hg > Papers > 2022 > soto-sigos

comparison Paper/soto-sigos.tex @ 3:952d4dbb7c6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP 仮完成
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 03:30:26 +0900
parents f9794e92f964
children 7434c0aa1859
comparison
equal deleted inserted replaced
2:f9794e92f964 3:952d4dbb7c6a
46 } 46 }
47 \usepackage{caption} 47 \usepackage{caption}
48 \newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em} 48 \newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em}
49 \captionsetup[lstlisting]{font={small, tt}} 49 \captionsetup[lstlisting]{font={small, tt}}
50 50
51 \renewcommand{\lstlistingname}{Code}
52
53
51 \begin{document} 54 \begin{document}
52 55
53 % Title, Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 56 % Title, Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
54 \title{GearsAgda上のモデル検査の形式化} 57 \title{GearsAgda上のモデル検査の形式化}
55 58
76 \input{tex/cbc.tex} % cbc の説明 軽く 79 \input{tex/cbc.tex} % cbc の説明 軽く
77 % \input{tex/agda.tex} % agda の説明　もしかしたらいるかも 80 % \input{tex/agda.tex} % agda の説明　もしかしたらいるかも
78 \input{tex/cbc_agda.tex}% Gears Agda の記法　loopのやつやる 81 \input{tex/cbc_agda.tex}% Gears Agda の記法　loopのやつやる
79 82
80 \section{モデル検査} 83 \section{モデル検査}
81 モデル検査の説明をする。 84 モデル検査とは、検証手法の一つである。
85 他の検証手法として代表的なものとして、定理証明が挙げられる
86
87 モデル検査はプログラムが入力に対して仕様を満たした動作を
88 行うことを網羅的に検証することを指す。
89
90 モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる
91 状態爆発が起こり得るという問題がある。
92 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
93 できるが、専門的な知識が多く難易度が高いという欠点がある。
82 94
83 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる 95 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
84 96
85 \section{DPPのモデル検査} 97 \section{DPPのモデル検査}
86 モデル検査の機能として、入力の網羅が挙げられる。 98 モデル検査の機能として、入力の網羅が挙げられる。
89 101
90 そのため、next-codeがthinkingかeatingであるものに対して分岐を網羅する Code \ref{agda-dpp-bruteforce} 102 そのため、next-codeがthinkingかeatingであるものに対して分岐を網羅する Code \ref{agda-dpp-bruteforce}
91 を定義した。 103 を定義した。
92 104
93 105
94 \lstinputlisting[caption= Gears Agdaでの DPP の 左のフォークを取るコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced} 106 \lstinputlisting[caption= Gears Agdaでの DPP の場合を網羅するコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced}
95 107
96 内部で行っていることとして、その Code Gear 内に存在している next-code が thinking もしくは eatingである場合に 108 内部で行っていることとして、その Code Gear 内に存在している next-code が thinking もしくは eatingである場合に
97 そのプロセスのnext-codeをそのままにするか、それぞれ pickup-rfork か putdown-lfork にする。 109 そのプロセスのnext-codeをそのままにするか、それぞれ pickup-rfork か putdown-lfork にする。
98 そのため、その部分に対してbit全探索を行い、場合の網羅を行っている。 110 そのため、その部分に対してbit全探索を行い、場合の網羅を行っている。
99 111