SE547: Sequential noninterference [7/23]

Model of commands (c₁, μ₁) (c₂, μ₂):

1. If (c₁, μ₁) μ₂ then (c₁d, μ₁) (d, μ₂)

2. If (c₁, μ₁) (c₂, μ₂) then (c₁d, μ₁) (c₂d, μ₂)

3. If μ(e) is nonzero then (if (e) {c} else {d}, μ) (c, μ)

4. If μ(e) is zero then (if (e) {c} else {d}, μ) (d, μ)

5. What about while?

Model of commands final step (c₁, μ₁) μ₂:

6. (x=e, μ) μ[x:=μ(e)]

7. What about while?

Example:

x:=1; while(x) { x=x-1; }