Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/akasha.tex @ 78:897fda8e39c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reconstruct paper
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 08 Feb 2017 14:49:51 +0900
parents 50c2d2f1a186
children c407b7403548
comparison
equal deleted inserted replaced
77:50c2d2f1a186 78:897fda8e39c5
229 この411回のうちの実行パスでは赤黒木の仕様は常に満たされる。 229 この411回のうちの実行パスでは赤黒木の仕様は常に満たされる。
230 しかし、この展開された回数は挿入された回数とは無関係であり、実際どの程度検証することができたか確認できない。 230 しかし、この展開された回数は挿入された回数とは無関係であり、実際どの程度検証することができたか確認できない。
231 実際、赤黒木に恣意的なバグを追加した際にも仕様の反例は得られず、CBMC で扱える範囲内では赤黒木の性質は検証できなかった。 231 実際、赤黒木に恣意的なバグを追加した際にも仕様の反例は得られず、CBMC で扱える範囲内では赤黒木の性質は検証できなかった。
232 232
233 よって、CBMCでは検証できない範囲の検証を akasha で行なえることが確認できた。 233 よって、CBMCでは検証できない範囲の検証を akasha で行なえることが確認できた。
234 しかし、要素数13個分の挿入を検証しても赤黒木の挿入が必ずバランスするとは言いづらい。 234
235 より大きな数を扱っても現実的な速度で検証が行なえる必要がある。 235 % }}}
236 そのためには記号化なので状態の抽象化や、何らかの機構により状態の削減を行なう必要がある。
237 CbC における状態の抽象化の内部表現や、状態を削減するための制約として、型に注目した。
238 特に、型を値として利用できる
239
240 % }}}