Hoare逻辑 n>=0 ∥一个简单的例子 function mult(m,n){ {(0=m×0)人(0<=n)} x=0; {(x=m×0)入(0<=n)} y=0; {(x=mxy)入(y<=n)} while y <n do {(x+m=m×(y+1)Λ(y+1)<=n)} x=x十m; {(x=m(y+1)Λ(y+1)<=n)} y=y+1; {(x=mxy)入(y<=n)} }x=m×n
Hoare逻辑 n >= 0 function mult(m, n) { { (0 == m0) (0 <= n) } x = 0 ; { (x == m0) (0 <= n) } y = 0 ; { (x == my) (y <= n) } while y < n do { { (x+m == m(y+1)) ((y+1) <= n) } x = x + m ; { (x == m(y+1)) ((y+1) <= n) } y = y + 1 ; { (x == my) (y <= n) } } } x = m n //一个简单的例子
最弱前条件演算 ·Dijkstra的思路 为了验证{P}C{Q},找出所有使得 {P}C{Q}的断言P,称为Pre(C,Q) 验证存在p∈Pre(C,Q)that P→P” 这些断言形成一个格 false true Pre(C,O 强 弱 最弱前条件WP(C,Q) 变成计算WP(C,Q)并且证明P→WP(C,2)
最弱前条件演算 • Dijkstra的思路 – 为了验证 { P } C { Q }，找出所有使得 { P } C { Q }的断言P，称为Pre(C, Q) – 验证存在P Pre(C, Q) that P P – 这些断言形成一个格 – 变成计算WP(C, Q)并且证明P WP(C, Q) false true 强 弱 Pre(C, Q) P 最弱前条件WP(C, Q)