Let BB = B1 ? B2 ? … ? Bn
Let BB = B1 ? B2 ? … ? Bn
H0(R) = ?BB ? R
- Represents the set of states in which execution of DO terminates in 0 iterations with R true, as the guards are initially false
wp(DO,R) = ?k: 0<=k: Hk(R)
- Represents the set of states in which execution of DO terminates in a bounded number of iterations with R true.
Example: What does the following calculate? How can we prove it?
i,s = 1, b[0];
Do i <> 11 ? i,s := i+1, s + b[i] OD
{R: s = ? k: 0<=k:b[k])}