5.3操作语义 如果想证明P,S→exec'S,需要观察P的语法形式，考 察哪条规则是完成该证明的最后一条规则 ·例 p:=0; m:=0; while(cont m≠ndo p :cont m; m :(cont m)+1; od
5.3 操作语义 • 如果想证明P, s →exec s ,需要观察P的语法形式,考 察哪条规则是完成该证明的最后一条规则 • 例 p := 0; m := 0; while (cont m) n do p := cont m; m := (cont m) +1; od
5.3操作语义 p:=0; S update s l,0 m:=0; while(cont m)≠ndo p :cont m; m :=(cont m)+1; od
5.3 操作语义 p := 0; s1 = updateA s l p 0 m := 0; while (cont m) n do p := cont m; m := (cont m) +1; od