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×nHoare逻辑 n >= 0 function mult(m, n) { { (0 == m0)  (0 <= n) } x = 0 ; { (x == m0)  (0 <= n) } y = 0 ; { (x == my)  (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 == my)  (y <= n) } } } x = m  n //一个简单的例子