5.3 操作语义 KB,s〉→eval false(Pz,S〉→exec S' if B then Pielsep2,s)->exec s' 〈B,s)-→eval false 〈while B do Pod,S〉→eees KB,s)-→eval true(P,s)→exec S'(while B do P od,.s'）→>exes' while B do Pod,.S〉-→exec S"'5.3 操作语义 B, s →eval false P2 , s →exec s if B then P1 elseP2 , s →exec s B, s →eval false while B do P od, s →exec s B, s →eval true P, s →exec s while B do P od, s →exec s while B do P od, s →exec s