证明程序的部分正确性

Question

下面是在数组中找到最大数的函数， 所以教授教我们证明部分正确性。 他给出了证明循环不变量保持不变的解决方案。 任何人都可以向我解释解决方案吗？

find_max (a: ARRAY [INTEGER]): INTEGER
   require
      not_empty: a.count > 0
   local
      i: INTEGER
   do
      from
         i := a.lower
         Result := a [i]
      invariant
            −− Predicate Equivalent: ∀j | a.lower ≤ j < i • Result ≥ a[j]
         across a.lower |..| (i − 1) as j all Result >= a [j.item] end
      until
         i > a.upper
      loop
            -- { ∀j ∣ a.lower ≤ j < i ● Result ≥ a [j] ∧ ¬(i > a.upper) }
         if a [i] > Result then
            Result := a [i]
         end
            -- { ∀j ∣ a.lower ≤ j < i ● Result ≥ a [j] }
         i := i + 1
      variant
         a.upper − i + 1
      end
   ensure
         −− Predicate Equivalent: ∀j | a.lower ≤ j ≤ a.upper • Result ≥ a[j]
      across ... all ... end
   end

解决方案。 我们首先计算循环体的wp 以保持 LI（循环不变量）：

   wp (if a[i] > Result then Result := a[i] end; i := i + 1, 
       ∀j | a.lower ≤ j ≤ i − 1 • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a [j])

= {wp rule for seq. comp. }
   wp (if a[i] > Result then Result := a[i] end, wp (i := i + 1,
       ∀j | a.lower ≤ j ≤ i − 1 • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a [j]))

= {wp rule for assignment}
   wp (if a[i] > Result then Result := a[i] end, 
       ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a [j]) 

= {wp rule for conditional}
   a [i] > Result =⇒ wp (Result := a[i], 
                         ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a [j])
   ∧
   a [i] ≤ Result =⇒ wp (Result := Result, 
                         ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a [j])

= {wp rule for assignment, twice}
   a [i] > Result =⇒ ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ a [i] ≥ a[j]
   ∧
   a [i] ≤ Result =⇒ ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a[j]

然后我们证明前提条件（即¬(exit condition)和LI）不弱于上面计算的wp：

¬(i > a.upper) ∧ ( ∀j | a.lower ≤ j ≤ i − 1 • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a[j] ) =⇒ a [i] > Result =⇒ 
   ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ a [i] ≥ a [j]


   ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ a [i] ≥ a [j]

≡ {split range: ∀j | a.lower ≤ j ≤ i • P (j) ≡ (∀j | a.lower ≤ j ≤ i − 1) ∧ P (i)}
  (∀j | a.lower ≤ j ≤ i - 1 • a.lower ≤ j ∧ j ≤ a.upper ∧ a[i] ≥ a[j]) ∧ 
                             (a.lower ≤ i ∧ i ≤ a.upper ∧ a[i] ≥ a[i])

≡ {antecedent: a[i] > Result; and RHS of precond: ∀j | a.lower ≤ j ≤ i − 1 • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a[j]}
   true ∧ (a.lower ≤ i ∧ i ≤ a.upper ∧ a[i] ≥ a[i])

≡ {LHS of precond: ¬(i > a.upper) and a[i] ≥ a[i] ≡ true}
  (Exercise )
  true

Answer 1

一般方案

1. 函数后置条件Q

   ∀j | a.lower ≤ j ≤ a.upper • Result ≥ a [j]
   

   可以从循环不变量L

   导出

   ∀j | a.lower ≤ j < i • Result ≥ a [j]
   

   通过考虑循环退出条件i > a.upper。假设i 在循环中每次迭代都会增加1，满足退出条件的第一个值是i = a.upper + 1。将此值代入 L 得到 Q。因此，在第一次迭代之前证明 L 为真并被循环保存就足够了。

2. 对于第一次迭代（i := a.lower 和 Result := a [i]），循环不变量变为

   ∀j | a.lower ≤ j < a.lower • Result ≥ a [j]
   

   这很正常（因为j 的范围是空的）。

3. 让我们找到循环的最弱前提条件，前提是在每次迭代结束时，L 应该为真。在循环内部，根据退出条件i ≤ a.upper，L相当于

   ∀j | a.lower ≤ j ≤ i − 1 • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a [j]
   

   反过来，使用最弱前置条件规则（见下文），可以简化为两个谓词的合取

   a [i] > Result =⇒ ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧  a [i] ≥ a[j]
   a [i] ≤ Result =⇒ ∀j | a.lower ≤ j ≤ i • a.lower ≤ j ∧ j ≤ a.upper ∧ Result ≥ a[j]
   

   如解决方案所示，第一个在不满足退出条件且循环不变量 L 在循环体之前为真的假设下简化为真。第二个谓词也可以这样做。

4. 考虑到 L 在循环的第一次迭代之前得到满足并且在每次迭代中都被保留，我们得出结论 L 在循环之后得到满足，因此，当函数返回时，Q 为真。

最弱前置条件规则

上述证明依赖于以下最弱的前置条件规则：

1. 顺序组合

   wp (S;T, P) = wp (S, wp (T, P))
   

2. 作业

   wp (x := e, P) = P [e/x]
   

3. 有条件的

   wp (if b then S else T end, P) = (b =⇒ wp (S, P)) ∧ (¬b =⇒ wp (T, P))
   

   解释。 b 的值事先是未知的。但是，如果我们假设b 为真，则整个指令归约为S，最弱的前置条件应该是wp (S, P)。事实上，当b 被上面公式中的True 替换时会发生这种情况（b =⇒ wp (S, P) 变为wp (S, P) 并且¬b =⇒ wp (T, P) 变为True，因此整个公式简化为wp (S, P)）。如果我们假设b 是False（第一部分变成True，第二部分变成wp (T, P)），类似的推理也适用。