Mercurial > hg > Papers > 2020 > soto-midterm

diff tex/spec.tex @ 8:27a6616b6683
fix
author: soto@cr.ie.u-ryukyu.ac.jp
date: Mon, 14 Sep 2020 19:58:10 +0900
parents: acad18934981
children: a8bc8c6b48bd
--- a/tex/spec.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/spec.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -1,7 +1,5 @@
 \section{検証手法}
-手法は模索中であり、大半が先行研究と同じ手法を考えている。
-本章では先行研究で述べられている検証手法について説明する。
-流れとしては、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
+現在提案している手法は、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に
 コマンドの部分的な正当性を導けることを前述した。
 その為、agdaでのcbcの検証は下図のようになる。
 流れを説明すると、