Quantified Assertions

For program $F$, we write quantified assertions

• <forall $s$ : $s$ in $F$ :: $\{p\}\; s\; \{q\}$>
• <exists $s$ : $s$ in $F$ :: $\{p\}\; s\; \{q\}$>

• <forall $s$ : $s$ in <[] $i$ : $b(i)$ :: $t(i)$> :: $\{p\}\; s\; \{q\}$>
  • Show $\{p$ and $b(i)\}\; t(i)\; \{q\}$.
• <exists $s$ : $s$ in <[] $i$ : $b(i)$ :: $t(i)$> :: $\{p\}\; s\; \{q\}$>
  • Show $\{p$ and $b(k)\}\; t(k)\; \{q\}$
    (for some $j$ with $b(j)$).