Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/tex/hoare.tex @ 2:9176dff8f38a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD while loop description
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 05 Nov 2021 15:19:08 +0900
parents c59202657321
children
comparison
equal deleted inserted replaced
1:3910f4639344 2:9176dff8f38a
14 Hoare Logic の検証では、 14 Hoare Logic の検証では、
15 「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。 15 「条件がすべて正しく接続されている」かつ「コマンドが停止する」ことが必要である。
16 これらを満たし、 16 これらを満たし、
17 事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 17 事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。
18 18
19 \section{Hoare Logic による Code Gear の検証手法 } 19 \subsection{Hoare Logic による Code Gear の検証手法 }
20 20
21 \figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。 21 \figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。
22 input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、 22 input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、
23 output DataGear が Post Conditionとなる。 23 output DataGear が Post Conditionとなる。
24 各DataGear が Pre / Post Condition を満たしているかの検証は、 24 各DataGear が Pre / Post Condition を満たしているかの検証は、