Floyd-Hoare Automata

有限状态自动机$A=(Q,\delta ,q_0,F)$如果满足：存在一个映射I，使得$q\in Q$被映射为断言${\varphi }_q$，且有：

1. $(q,st,q^{\prime })\in \delta ⟹\{{\varphi }_q\}st\{\varphi {}_{q^{\prime }}\}$
2. $q=q_0⟹{\varphi }_{pre}\models {\varphi }_q$
3. $q\in F⟹{\varphi }_q\models {\varphi }_{post}$

则A是Floyd-Hoare Automata. 映射I称为annotation

Floyd-Hoare Automata 只接受正确的trace