proof - 证明形式逻辑的正确性

Question

我想知道是否有人可以帮我回答这个问题。它来自以前的试卷，我可以为今年的考试准备好答案。

这个问题看起来太简单了，我完全迷路了，它到底在问什么？

Consider the following section of code involving integer variables:

if (i < j) {
    m = i;
} else {
    m = j;
}

By stating an appropriate output condition and then verifying thecorrectness of the piece of code, prove that after execution, m is equal tothe minimum of i and j.

我的发布条件为:{m = i ∧ i < j ∨ m = j ∧ j < i}

这是正确的吗？你如何验证这一点？

Answer 1

您的帖子条件是正确的。不过，我个人认为以下变体(等效)更自然:

(i<j → m=i) ∧ (i≥j → m=j)

要证明程序满足发布条件，请执行以下操作。

1. 请注意，要确保程序始终 满足发布条件，您应该使用true。作为你的先决条件。

2. 所以你有以下霍尔三元组:

   {true}
   if (i < j) {
   
   
       m = i;
   
   } else {
   
   
       m = j;
   
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

3. 后置条件需要在两个分支的末尾都成立，所以(根据条件的标准最弱前置条件规则)我们有

   {true}
   if (i < j) {
   
   
       m = i;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--.
   } else {                                       |
                                                  |
                                                  |
       m = j;                                     |   copy
       {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--|
   }                                              |
   {(i < j → m = i) ∧ (i ≥ j → m = j)}  ----------'
   

4. 根据赋值 yield 的最弱前提条件进一步推高公式

   {true}
   if (i < j) {
   
       {(i < j → i = i) ∧ (i ≥ j → i = j)}   <---.
       m = i;                                    | m replaced by i
       {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
   } else {
   
       {(i < j → j = i) ∧ (i ≥ j → j = j)}   <---.
       m = j;                                    | m replaced by j
       {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

5. 在真实分支的顶部我们知道 i < j ，在 else 分支的顶部我们知道 ¬(i < j) :

   {true}
   if (i < j) {
       {i < j}                               (1)  <--- added
       {(i < j → i = i) ∧ (i ≥ j → i = j)}   (2)
       m = i;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}
   } else {
       {¬(i < j)}                            (3)  <--- added
       {(i < j → j = i) ∧ (i ≥ j → j = j)}   (4)
       m = j;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

6. 剩下要显示的是对于任何两个连续的断言，第一个断言意味着第二个断言。 (这些通常被称为“证明义务”。)我们有两个这样的义务:(1)应该暗示 (2)和 (3)应该暗示(4) .显然是这样。

   -- "qed":-)