Mercurial > hg > Papers > 2023 > soto-master
diff Paper/tex/tree_desc.tex @ 22:b37e4cd69468
Add slide
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Feb 2023 16:35:38 +0900 |
| parents | 785dd684c529 |
| children |
line wrap: on
line diff
--- a/Paper/tex/tree_desc.tex Fri Feb 03 19:06:13 2023 +0900 +++ b/Paper/tex/tree_desc.tex Sun Feb 05 16:35:38 2023 +0900 @@ -87,10 +87,10 @@ 条件としている。 これを先ほど実装した CodeGear に対して加えることで検証していく。 -先ほど実装した \coderef{bt_find_impl} に対して加えると \coderef{bt_invariant} のようになる。 +先ほど実装した \coderef{bt_find_impl} に対して加えると \coderef{bt_invariant2} のようになる。 -\lstinputlisting[label=code:bt_invariant, caption=Binary Tree の検証] {src/bt_verif/find.agda.replaced} +\lstinputlisting[label=code:bt_invariant2, caption=Binary Tree の検証] {src/bt_verif/find.agda.replaced} 現時点では条件を満たしていることの証明まで行っていないが コード中の {!!} に記述を行い、前述した While Loop と同じように中身を記述することで検証を行える。