5.3 操作语义 5.3.2命令的执行 命令的执行可以用关系→>c来刻画 (M,S〉-→evat V updateA(s,n(x),v)=s' K:=M,S〉-→exec S KP1,S〉-→exec S'(P2,s'〉→exec S" 〈P1;P2z,S〉-→exec S” KB,S〉-→eval true〈Pi,S〉-→exec S' (if B then P1 elseP2,S〉→exes5.3 操作语义 5.3.2 命令的执行 命令的执行可以用关系→exec来刻画 updateA(s, (x), v)=s M, s →eval v x := M, s →exec s P1 , s →exec s P2 , s →exec s  P1 ;P2 , s →exec s B, s →eval true P1 , s →exec s if B then P1 elseP2 , s →exec s