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

Question

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

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？

考虑以下涉及整数变量的代码部分：

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

通过陈述一个合适的输出条件，然后验证这段代码的正确性，证明执行后m等于i和j的最小值。

我的后置条件为：{m = i ∧ i < j ∨ m = j ∧ j < i}

它是否正确？你如何验证这一点？

Answer 1

您的帖子条件是正确的。我个人发现以下变体（等效）更自然：

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

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

1. 请注意，要确保程序始终满足后置条件，您应该将true其用作前置条件。

2. 所以你有以下 Hoare 三元组：

   {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. 根据分配产生的最弱前提条件将公式进一步推高

   {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. 在 true 分支的顶部，我们知道，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”:-)