Archive:

Hoare 逻辑


Hoare 逻辑是一种证明程序性质的有效方法,它包含了两种为程序撰写规范的想法。

  1. 自然的书写程序规范的范式。
  2. 结构化的证明技术。

Assertion 断言

断言是关于内存当前状态的一种描述,我们可以使用断言来描述程序的规范。

下面是断言的定义以及一些例子。

Definition Assertion := State -> Prop.
fun st => st X = 3.
fun st => True.

Hoare 三元组

Hoare 三元组是一个关于程序运行一条指令前后状态的描述,它可以被写成下面的形式。

{P} c {Q}

这代表着,

  1. 如果指令 c 执行时,内存状态满足断言 P
  2. 并且指令 c 最终结束执行,抵达终止状态。
  3. 那么这个终止状态满足断言 Q

下面是 Hoare 三元组的形式化定义。

Definition hoare_triple
            (P : Assertion) (c : com) (Q : Assertion) : Prop :=
  forall st st'
    st =[ c ]=> st' ->
    P st ->
    Q st'.

证明规则

Hoare 逻辑可以提供一种“组合式”的证明方法,使证明能够反映出程序自身的结构。最终,我们能够实现直接利用这些规则来证明程序的性质而不需要对 hoare_triple 进行展开。

Assignment 赋值规则

{Q [X |-> a]} X := a {Q}

这意味着,若 QX |-> a 的情况下成立,那么在它被赋值为 a 后,Q 仍然成立。

Consequence 结果规则

时常,我们会遇到已有条件 P 强于我们需要的条件 P' 的情况,既 P ->> P'。这时我们需要将所需条件中的 P' 替换成 P 这就需要结果规则。

替换前置条件 P

{P'} c {Q} ->
P ->> P' ->
{P} c {Q}

替换后置条件 Q

{P} c {Q'} ->
Q' ->> Q ->
{P} c {Q}

Sequencing 序列规则

当两条指令 c1; c2 顺序执行时,我们可以引入顺序规则。

{P} c1 {Q} ->
{Q} c2 {R} ->
{P} c1; c2 {R}

Conditionals 条件规则

为了证明条件语句 if 的性质,我们需要添加一条规则,例如下面这个“过强”的规则。

{P} c1 {Q} ->
{P} c2 {Q} ->
{P} if b then c1 else c2 end {Q}

其要求只有 c1c2 均满足时,我们才能推出上面的结果,但大多数情况下,我们其实是已经知道关于 b 的知识,例如 b = true 等, 要利用上 b 我们必须弱化前提,来使定理强化。

{P /\ b} c1 {Q} ->
{P /\ ~ b} c2 {Q} ->
{P} if b then c1 else c2 end {Q}

为什么这种修改使得整个规则“强化”了呢?

注意到,我们实际上加强了三元组中的“初始状态”,我们对初始状态要求的更多了,等于弱化了前提,使得我们能够利用 b 的性质来抵消掉前提中的某一条。 例如我们如果已经知道 b = true,那么我们可以让 {P /\ ~ b} c2 {Q} 直接弱化成 true,具体过程如下。

st =[ c2 ]=> st' ->
(P /\ ~ b) st ->
Q st'

根据 c2 的终止情况,我们可以判断出,若 c2 不终止,则该三元组直接为真,若 c2 终止,该三元组变为 (P /\ b) st -> Q st'

根据 b = true,我们可以判断出,(P /\ ~ b) = false,该三元组直接为真。

因此我们成功利用 b 的知识舍去了一个前提。

While 循环规则

基于同样的规则,我们可以提出 while 的推导规则。

{P /\ b} c {P} ->
{P} while b do c end {P /\ ~ b}

装饰程序

Hoare 逻辑的最大优点是可以将程序和其证明的结构组合起来(compositional)。但是为程序构造合适的证明是困难的,我们通常可以 使用迭代的方式,即从显然的条件(True/False)出发,一步步构造出正确的证明。

例子:两数交换

X := X + Y;
Y := X - Y;
X := X - Y

它有下面的装饰证明。

{ X = m /\ Y = n } ->>            (* algebra *)
{ (X + Y) - ((X + Y) - Y) = n /\ (X + Y) - Y = m }
X := X + Y;                       (* [X |-> X + Y] *)
{ X - (X - Y) = n /\ X - Y = m }  (* [Y |-> X - Y] *)
Y := X - Y;
{ X - Y = n /\ Y = m }            (* [X |-> X - Y] *)
X := X - Y
{ X = n /\ Y = m }

上面的证明通过下面的步骤构造而成。

  1. 在程序起始和末尾加上我们“期望”程序表现的行为。既 { X = m /\ Y = n }{ X = n /\ Y = m }
  2. 由 Hoare 逻辑的赋值规则从后向前倒推,直到第一行。
  3. 通过化简将起始条件转换成所需条件,”-»“。

例子:简单条件语句

if X <= Y then
  Z := Y - X
else
  Z := X - Y
end

我们同样也可以为其构造装饰证明。

{ True }
if X <= Y then
  { True /\ X <= Y } ->> { (Y - X) + X = Y \/ (Y - X) + Y = X } (* left *)
  Z := Y - X
  { Z + X = Y \/ Z + Y = X }
else
  { True /\ ~ (X <= Y) } ->> { (X - Y) + X = Y \/ (X - Y) + Y = X } (* right *)
  Z := X - Y
  { Z + X = Y \/ Z + Y = X }
end
{ Z + X = Y \/ Z + Y = X }

上面的证明也是采用相同的步骤。

例子:除法

X := m
Y := 0
while n <= X do
  X := X - n
  Y := Y + 1
end;

为了给该程序提供一个证明,我们需要记住除法的性质,既 n × Y + X = m /\ X < n。 幸运的是,该 Prop 左边就是我们需要的循环不变量。以此为基础构造证明即可。

练习:寻找不变量

while ~ (X = 0) do
  Z := Z + 1;
  X := X - 1
end
  • 添加期望条件
{ X = m /\ Y = n}
while ~ (X = 0) do
  Z := Z + 1;
  X := X - 1
end
{ Y = m + n }
  • 添加基础不变量
{ X = m /\ Y = n } ->> { True }
while ~ (X = 0) do
  { True /\ X <> 0 }            (* ok *)
  Y := Y + 1;
  { True }                      (* ok *)
  X := X - 1
  { True }                      (* ok *)
end
{ True /\ X = 0 } ->> { Y = m + n } (* wrong *)
  • 尝试收紧不变量
{ X = m /\ Y = n } ->> { Y = m + n }
while ~ (X = 0) do
  { Y = m + n /\ X <> 0 }            (* wrong *)
  Y := Y + 1;
  { Y = m + n }                      (* wrong *)
  X := X - 1
  { Y = m + n }                      (* wrong *)
end
{ Y = m + n /\ X = 0 } ->> { Y = m + n } (* ok *)

看起来我们需要将 X 纳入考量范围。

  • 更改不变量,考虑 X
{ X = m /\ Y = n } ->> { Y + 1 = m + n - ( X - 1 )  } (* ok algebra *)
while ~ (X = 0) do
  { Y + 1 = m + n - (X - 1) /\ X <> 0 }               (* ok *)
  Y := Y + 1;
  { Y = m + n - (X - 1) }                             (* ok *)
  X := X - 1
  { Y = m + n - X }                                   (* ok *)
end
{ Y = m + n - X /\ X = 0 } ->> { Y = m + n }          (* ok algebra *)
  • 重写成好看的形式 X + Y = m + n
{ X = m /\ Y = n } ->> { X + Y = m + n  }             (* ok algebra *)
while ~ (X = 0) do
  { (X - 1) + (Y + 1) = m + n /\ X <> 0 }             (* ok *)
  Y := Y + 1;
  { (X - 1) + Y = m + n }                             (* ok *)
  X := X - 1
  { X + Y = m + n }                                   (* ok *)
end
{ X + Y = m + n /\ X = 0 } ->> { Y = m + n }          (* ok algebra *)

练习:阶乘

{ X = m }
Y := 1;
while ~ ( X = 0 ) do
  Y := Y * X ;
  X := X - 1
end  
{ Y = m! }

下面是一次失败尝试,看起来是 (X + 1) * Y = m! 的右侧常量条件过强,应当调整为随循环变化的量。

{ X = m }
Y := 1;
{ X = m /\ Y = 1 }
while ~ ( X = 0 ) do
  { X = 1 /\ X * (X * Y) = m! }              (* wrong *)
  Y := Y * X ;
  { X - 1 = 0 /\ X * Y = m! }
  X := X - 1
  { X = 0 /\ (X + 1) * Y = m! }
end
{ X = 0 /\ (X + 1) * Y = m! } ->> { Y = m! } (* ok algebra *)

又一次失败尝试,看起来 /\ 右侧的条件可以了,但是左侧的 X 递减的性质没有体现出来。

{ X = m }
Y := 1;
{ X = m /\ Y = 1 }
while ~ ( X = 0 ) do
  { X = 1 /\ X * Y * X = Y * X }
  Y := Y * X ;
  { X = 1 /\ X * Y = Y }
  X := X - 1
  { X = 0 /\ (X + 1) * Y = Y }
end  
{ X = 0 /\ (X + 1) * Y = Y } ->> { Y = m! }

舍弃对 X 的常数约束,改为利用阶乘性质约束 X! * Y = m!

这一点从循环的性质可以得到,例如

  1. 最后一次循环,我们有 Y = 1*2...*m /\ X = 0
  2. 倒数第二次循环,我们有 Y = 2*...*m /\ X = 1
  3. 倒数第三次循环,我们有 Y = 3*...*m /\ X = 2
{ X = m } ->> { X = m /\ 1 = 1 }
Y := 1;
{ X = m /\ Y = 1 }
while ~ ( X = 0 ) do
  { X = m /\ Y = 1 /\ ~ (X = 0) } ->>
  { (X - 1)! * Y * X = m! }
  Y := Y * X ;
  { (X - 1)! * Y = m! }
  X := X - 1
  { X! * Y = m! }
end  
{ X! * Y = m! /\ X = 0 } ->> { Y = m! }

例子:幂级数

X := 0;
Y := 1;
Z := 1;
while ~ (X = m) do
  Z := 2 * Z;
  Y := Y + Z;
  X := X + 1
end
  • 起始和终止条件。
{ True } ->> { 0 = 0 }
X := 0;
{ X = 0 } ->> { X = 0 /\ 1 = 1 }
Y := 1;
{ X = 0 /\ 1 = 1 } ->> { X = 0 /\ Y = 1 /\ 1 = 1 }
Z := 1;
{ X = 0 /\ Y = 1 /\ Z = 1 }
while ~ (X = m) do
  Z := 2 * Z;
  Y := Y + Z;
  X := X + 1
end
{ Y = 2 ^ (m + 1) - 1 }
  • 观察规律,得到
  1. 最后一次循环,Y = 1 + 2 + 2 ^ 2 + ... + 2 ^ m /\ X = m /\ Z = 2 ^ m
  2. 倒数第二次循环,Y = 1 + 2 + 2 ^ 2 + ... + 2 ^ (m - 1) /\ X = m - 1 /\ Z = 2 ^ (m - 1)
  3. 倒数第三次循环,Y = 1 + 2 + 2 ^ 2 + ... + 2 ^ (m - 2) /\ X = m - 2 /\ Z = 2 ^ (m - 2)
{ True } ->> { 0 = 0 }
X := 0;
{ X = 0 } ->> { X = 0 /\ 1 = 1 }
Y := 1;
{ X = 0 /\ 1 = 1 } ->> { X = 0 /\ Y = 1 /\ 1 = 1 }
Z := 1;
{ X = 0 /\ Y = 1 /\ Z = 1 }
while ~ (X = m) do
  { X = 0 /\ Y = 1 /\ Z = 1 } ->>         (* ok algebra *)
  { 2 * Z + Y = 2 ^ ((X + 1) + 1) - 1 }
  Z := 2 * Z;
  { Z + Y = 2 ^ ((X + 1) + 1) - 1 }       (* ok *)
  Y := Y + Z;
  { Y = 2 ^ ((X + 1) + 1) - 1 }           (* ok *)
  X := X + 1
  { Y = 2 ^ (X + 1) - 1 }                 (* ok *)
end
{ X = m /\ Y = 2 ^ (X + 1) - 1 } ->>      (* ok end condition *)
{ Y = 2 ^ (m + 1) - 1 }

最弱前提

最弱前提的非形式定义如下。

  1. P 是一个前提,{ P } c { Q }
  2. P 至少和其他所有前提一样弱,{ P' } c { Q } -> P' ->> Q

其形式化定义如下。

Definition is_wp P c Q :=
  { P } c { Q } /\
  forall P', { P' } c { Q } -> (P' ->> P).

Hoare 逻辑与理论模型

Hoare 逻辑描述了所有可能的三元组,但与现实模型不同的地方在于,所有可以被三元组描述出来的程序中, 只有一部分是合法的(valid)。

因此我们需要定义出所有合法的三元组。

Definition valid (P : Assertion) (c : com) (Q : Assertion) : Prop :=
  forall st st',
    st =[ c ]=> st' ->
    P st ->
    Q st.

与此同时,如果将 Hoare 逻辑看成一组逻辑系统,我们也可以同样得到一组 derivation rules,来 对 Hoare 三元组进行操作。

image.png

形式化的定义如下。

Inductive derivable : Assertion -> com -> Assertion -> Type :=
  | H_Skip : forall P,
      derivable P <{skip}> P
  | H_Asgn : forall Q V a,
      derivable (Q [V |-> a]) <{V := a}> Q
  | H_Seq  : forall P c Q d R,
      derivable P c Q -> derivable Q d R -> derivable P <{c;d}> R
  | H_If : forall P Q b c1 c2,
    derivable (fun st => P st /\ bassn b st) c1 Q ->
    derivable (fun st => P st /\ ~(bassn b st)) c2 Q ->
    derivable P <{if b then c1 else c2 end}> Q
  | H_While : forall P b c,
    derivable (fun st => P st /\ bassn b st) c P ->
    derivable P <{while b do c end}> (fun st => P st /\ ~ (bassn b st))
  | H_Consequence  : forall (P Q P' Q' : Assertion) c,
    derivable P' c Q' ->
    (forall st, P st -> P' st) ->
    (forall st, Q' st -> Q st) ->
    derivable P c Q.

正确性与完备性

对于一个逻辑系统有上面两个概念 合法(valid)可推导(derivable)

  • 前者指该系统中所有合法的语句,是基于状态的。
  • 后者则是指该系统所有能够推导出的语句,是基于过程和推导树的。

我们怎样判断两种概念是一致的呢?这就涉及到下面的正确完备两种性质。

  • 正确性:所有能够推导出的语句都是合法的。
  • 完备性:所有合法的语句都是可以推导出的。