Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/master_paper.tex @ 13:62d87fdd7775

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add intro
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Tue, 31 Jan 2023 16:31:53 +0900
parents 3aa9d35e93bf
children f52e5fd41f58
comparison
equal deleted inserted replaced
12:3aa9d35e93bf 13:62d87fdd7775
127 \input{tex/hoare.tex} 127 \input{tex/hoare.tex}
128 \input{tex/while_loop.tex} % while loop の実装と検証(簡単に) 128 \input{tex/while_loop.tex} % while loop の実装と検証(簡単に)
129 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計 129 \input{tex/tree_desc.tex}% Gears Agda における木構造の設計
130 130
131 \input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる 131 \input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる
132 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる 132 % \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
133 133
134 \chapter{まとめと今後の展望} 134 \chapter{まとめと今後の展望}
135 本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。 135 本論文では Gears Agda による形式手法を用いたプログラムの検証について述べた。そこで、定理証明については Invariant を用いて定理証明を行った。モデル検査については Gears Agda にて dead lock を検知できるようになった。
136 136
137 実際に Invariant を用いることで、プログラムに与える入力とその出力に対して条件を与え、Hoare Logic による検証を行えるようになった。 137 実際に Invariant を用いることで、プログラムに与える入力とその出力に対して条件を与え、Hoare Logic による検証を行えるようになった。