算法正确性证明

发表于 | 更新于 | 分类于 | 评论数： | 阅读次数：
本文字数： 1k | 阅读时长 ≈ 0:01

例子

抽象例子

1
2
3
4
5
6
7
8
9
10
Procedure ALG
    #P
    Init
    #I
    while C
        #I and C
        S
    #I and not C
    Follow
    #Q
  • 目标：P{ALG}QP\{ALG\}Q
  • 途径：
    1. P{Init}IP\{Init\}I
    2. (I∧C){S}I(I\wedge C)\{S\}I
    3. (I∧¬C){Follow}Q(I\wedge \neg C)\{Follow\}Q
  • 注意
    • 循环不变量不唯一但强度不同

实际例子

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
equal(S1,S2)
    #P
    X=S1
    Y=S2
    E=true
    #I
    while X!=null && Y!=null && E
        if eq(head(X),head(Y))
            X=tail(X)
            Y=tail(Y)
        else
            E=false
    #A
    if !(X==null && Y==null)
        E=false
        #B
    else
        #C
    return E

不变量

  • P:(S1isstring)∧(S2isstring)P: (S_1 is string)\wedge(S_2 is string)
  • I:S1=S2⇔E∧X=YI: S_1=S_2 \Leftrightarrow E\wedge X=Y
  • A:I∧(X==null∨Y==null∨¬E)A: I\wedge (X==null \vee Y==null \vee \neg E)
  • B:A∧¬(X==null∧Y==null)B: A\wedge \neg (X==null \wedge Y==null)
  • C:A∧X==null∧Y==nullC: A\wedge X==null \wedge Y==null
  • Q:S1=S2⇔EQ: S_1=S_2 \Leftrightarrow E

证明内容

  • P⇒I1P \Rightarrow I_1
  • I1⇒I1I_1 \Rightarrow I_1
  • I1⇒I2I_1 \Rightarrow I_2
  • I2⇒I3I_2 \Rightarrow I_3
  • I2⇒I4I_2 \Rightarrow I_4
  • (I3⇒Q)∧(I4⇒Q)(I_3 \Rightarrow Q) \wedge (I_4 \Rightarrow Q)
0%