Elementary blocks A statement consists of a set of elementary blocks blocks Stmt P(Blocks) blocks([x :a])={[x:=a]} blocks([skip])={[skip]e} blocks(S1;S2)=blocks(S1)U blocks(S2) blocks(if [b]e then S1 else S2)={[b]e}Ublocks(S1)U blocks(S2) blocks(while [b]t do s)={[b]tU blocks(S) A statement s is label consistent if and only if any two elementary statements [S1]and [S2]with the same label in S are equal:S1=S2 A statement where all labels are unique is automatically label consistent PPA Section 2.1 C F.Nielson H.Riis Nielson C.Hankin (May 2005) 8Elementary blocks A statement consists of a set of elementary blocks blocks : Stmt → P(Blocks) blocks([x := a] ` ) = {[x := a] ` } blocks([skip] ` ) = {[skip] ` } blocks(S1; S2) = blocks(S1) ∪ blocks(S2) blocks(if [b] ` then S1 else S2) = {[b] ` } ∪ blocks(S1) ∪ blocks(S2) blocks(while [b] ` do S) = {[b] ` } ∪ blocks(S) A statement S is label consistent if and only if any two elementary statements [S1] ` and [S2] ` with the same label in S are equal: S1 = S2 A statement where all labels are unique is automatically label consistent PPA Section 2.1 c F.Nielson & H.Riis Nielson & C.Hankin (May 2005) 8