assume语句

如果从操作语义的视角来看，assume b如果在一个满足条件b的状态s下执行，则下一状态仍然是s，此时assume语句没有实际的效果；如果是在不满足条件b的状态下执行，执行流将终止。

用霍尔三元组来考察，规则如下： ${ϕ} assume b {ψ}$ 成立，当且仅当 $ϕ \land b ⟹ ψ$ 。可以这么理解：assume b从 $ϕ$ 中过滤出满足b的状态。最强后置条件就是 $ϕ \land b$ 。

并发场景

在实际的并发程序验证和分析工具中存在一个问题，即assume语句的语义是从线程局部还是全局进行解释。

尤其是在原子块和临界区（锁）之中的assume，因为这类构造的语义依赖于其正确地终止，此时assume的行为需要详细讨论。（WIP）

以上情况在实际遵从结构化编程的程序中不存在¹，因为分支和循环等构造等价的形式中assume总会对应互斥的两种情况，即transition system总是有后继的。上述情况会出现在为进行验证而插桩/建模的场景。