Hoare 逻辑

Hongyi Lu (jwnhy) Feb 10, 2022

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

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

Assertion 断言

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

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

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

Hoare 三元组

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

{P} c {Q}

这代表着，

如果指令 c 执行时，内存状态满足断言 P。
并且指令 c 最终结束执行，抵达终止状态。
那么这个终止状态满足断言 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}

这意味着，若 Q 在 X |-> 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}

其要求只有 c1 和 c2 均满足时，我们才能推出上面的结果，但大多数情况下，我们其实是已经知道关于 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 }

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

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

例子：简单条件语句

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!。

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

最后一次循环，我们有 Y = 1*2...*m /\ X = 0
倒数第二次循环，我们有 Y = 2*...*m /\ X = 1
倒数第三次循环，我们有 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 }

观察规律，得到

最后一次循环，Y = 1 + 2 + 2 ^ 2 + ... + 2 ^ m /\ X = m /\ Z = 2 ^ m。
倒数第二次循环，Y = 1 + 2 + 2 ^ 2 + ... + 2 ^ (m - 1) /\ X = m - 1 /\ Z = 2 ^ (m - 1)。
倒数第三次循环，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 }

最弱前提

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

P 是一个前提，{ P } c { Q }。
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 三元组进行操作。

形式化的定义如下。

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），

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

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

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