Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/spec.tex @ 8:27a6616b6683

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author soto@cr.ie.u-ryukyu.ac.jp
date Mon, 14 Sep 2020 19:58:10 +0900
parents acad18934981
children a8bc8c6b48bd
comparison
equal deleted inserted replaced
7:acad18934981 8:27a6616b6683
1 \section{検証手法} 1 \section{検証手法}
2 手法は模索中であり、大半が先行研究と同じ手法を考えている。 2 現在提案している手法は、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
3 本章では先行研究で述べられている検証手法について説明する。
4 流れとしては、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
5 コマンドの部分的な正当性を導けることを前述した。 3 コマンドの部分的な正当性を導けることを前述した。
6 その為、agdaでのcbcの検証は下図のようになる。 4 その為、agdaでのcbcの検証は下図のようになる。
7 流れを説明すると、 5 流れを説明すると、
8 CodeGear の引数となる DataGear が事前条件となり、 6 CodeGear の引数となる DataGear が事前条件となり、
9 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 7 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。