3. Secure Information Flow Analysis

if � � if [b] l then S1 else S2, σ � � →� � S1, σ � � , if B�b � σ = true if � � if [b] l then S1 else S2, σ � � →� � S2, σ � � , if B�b � σ = false wh � � while [b] l do S, σ � � → � � S; while [b] l do S,σ � � , if B�b � σ = true