第5章-命令式程序的语义-精选版.ppt

5.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 P1elseP2, s? ?exec s? * 5.3 操作语义 ?B, s? ?eval false ?P2, s? ?exec s? ?if B then P1elseP2, 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?? * 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; s1 = updateA s lp 0 m := 0; while (cont m) ? n do p := cont m; m := (cont m) +1; od * 5.3 操作语义 p := 0; s1 = updateA s lp 0 m := 0; s2 = updateA s1 lm 0 while (cont m) ? n do p := cont m; m := (cont m) +1; od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do p := cont m; m := (cont m) +1; od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do ?(cont m) ? n, s2? ?eval true p := cont m; m := (cont m) +1; od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do p := cont m; m := (cont m) +1; ?(p := cont m; m := (cont m) +1), s2? ?exec s3 od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do p := cont m; m := (cont m) +1; lookupA s3 lp = 0 lookupA s3 lm = 1 od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do ?(cont m) ? n, s3? ?eval true p := cont m; m := (cont m) +1; lookupA s3 lp = 0 lookupA s3 lm = 1 od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do p := cont m; m := (cont m) +1; lookupA s3 lp = 0 lookupA s3 lm = 1 ?(p := cont m; m := (cont m) +1), s3? ?exec s4 od * 5.3 操作语义 p := 0; m := 0; lookupA s2 lm = lookupA s2 lp = 0 while (cont m) ? n do p := cont m;