编程符号与递归程序的深入解析

### 编程符号与递归程序的深入解析 #### 1. 前置条件与不变式 在程序设计中，前置条件和不变式是确保程序正确性的重要概念。例如，对于某个程序，若要证明 `w = 29` 是 `p(a, b)` 的不变式，仅使用 `{ w = 29 } p(a, b) { w = 29 }` 是不够的，还需要额外的约束条件 `a ≠ 0`，即 `{ w == 29 ∧ a ≠ 0 } p(a, b) { w = 29 }`。这是因为当 `a < 0` 时，该程序可能无法终止。 #### 2. 参数传递方式 程序中的参数传递有不同的实现方式，主要涉及引用参数和值结果参数。 - **值结果参数**：在过程入口处，需要将实际参数 `b` 的值复制给形式参数 `y`；在过程出口处，再将 `y`（可能已被修改）的值复制回 `b`。 - **引用参数**：在过程入口处，将 `b` 的地址存储在 `y` 中。在过程体执行期间，对 `y` 的每次引用都被视为对 `b` 的间接引用。例如，在语句 `S` 中对 `y` 进行赋值，会立即对 `b` 进行赋值。过程出口处无需进行任何操作。 引用参数的优点是无需进行复制操作，这在 `y` 是大型数据结构（如大矩阵）时尤为重要；缺点是每次引用需要更多的时间。如果实际参数 `b` 不是过程体检查或修改的全局变量之一，那么证明规则适用于这两种实现方式。如果有多个引用参数，它们应该两两不同，并且都应与过程体检查或修改的全局变量不同。 #### 3. 递归程序 递归是程序设计中一种强大的技术，虽然所有递归程序都可以不使用递归的方式编写，但递归解决方案通常更加优雅和高效。然而，递归也带来了一些问题，例如对于所有条件 `U` 和 `V`，`{ U } p(x, y) { V }` 可能满足所有形式要求，但程序执行可能会陷入无限递归，无法终止于满足 `V` 的状态。 为了解决递归程序的终止问题，我们引入了边界函数，用于限制递归调用的次数。这类似于循环中引入边界函数来限制迭代次数。 下面通过一个邮票组合问题来展示递归程序的应用。美国邮政出售 `N` 种不同的邮票，第 `i` 种邮票的面值为 `v[i]`，`v[1..N]` 是一个给定的不同正整数数组。给定需要贴在信件上的一定金额，计算用这些邮票组成该金额的不同方式有多少种。 设 `c(x, n)` 表示用第 1 到第 `n` 种邮票组成金额 `x` 的组合数，其中 `x ≥ 0`，`0 ≤ n ≤ N`。函数 `c` 满足以下条件： - `c(0, n) = 1`，对于所有 `n`； - `c(x, 0) = 0`，对于 `x > 0`； - `c(x, n) = (∑ i : 0 ≤ i · v[n] ≤ x : c(x - i · v[n], n - 1))`，对于 `n > 0 ∧ x > 0`。 以下是实现该功能的程序： ```plaintext procedure p(x, n : integer; var y : integer); { x = x' ≥ 0 ∧ 0 ≤ n = n' ≤ N ∧ y = y' } [ var k : integer; [ X = 0 -> y := y + 1 | x > 0 ∧ n = 0 -> skip | x > 0 ∧ n > 0 -> k := 0; { inv : y = y' + (∑ i : 0 ≤ i < k : c(x - i · v[n], n - 1)) ∧ k ≥ 0 ∧ (k - 1) · v[n] ≤ x } { bf : x div v[n] - k } *[k · v[n] ≤ x -> p(x - k · v[n], n - 1, y); k := k + 1] { y = y' + c(x', n') } ``` 该递归是定义良好的，因为参数 `n` 由于前置条件（包括 `n ≠ 0`）而有下界，并且在递归调用中 `n` 的值会减小（变为 `n - 1`）。计算 `c(x, N)` 的问题可以通过以下语句解决： ```plaintext y := 0; p(x, N, y) { y = c(x, N) } ``` #### 4. 相关概念的历史与定义 - **Hoare 三元组**：由 [Hoa69] 引入，本文中 `{ P } S { Q }` 表示如果从满足 `P` 的初始状态开始执行语句 `S`，则执行保证会终止，并且最终状态满足 `Q`。Hoare 原始论文中的 `P {S} Q` 表示如果从满足 `P` 的初始状态开始执行语句 `S`，则执行可能终止也可能不终止；如果终止，最终状态满足 `Q`，这种版本有时被称为部分正确性，而本文关注的是完全正确性。 - **最弱前置条件**：通常我们感兴趣的是使 `{ P } S {Q }` 成立的最弱前置条件 `P`，根据 [Dij75]，将其写为 `wp(S, Q)`。该论文还引入了受保护命令。使 `P { S} Q` 成立的最弱前置条件 `P` 被称为最弱自由前置条件 `wlp(S, Q)`。`wp` 和 `wlp` 在 [Dij76] 中都有研究。 - **断言的思想**：通常归功于 [Flo67]，其基本思想也可以在 [Tur49] 中找到。可以参考 [Apt81] 了解通过 Hoare 三元组定义程序语义的概述及相关工作，参考 [Jon92] 了解历史概述。 #### 5. 练习题 以下是一些练习题，涵盖了最弱表达式、最强表达式、最弱前置条件、赋值语句、Hoare 三元组的证明等多个方面： 1. 给出在以下每种情况下可以替换省略号的最弱表达式： - `{ ... } X := X + 1 { X = 24 }` - `{ ... } X := X + 1 { x² > 45 }` - `{ ... } X := X + 1 { X² - X > 87 }` - `{ ... } X := x² - X + 1 { X ≥ 23 }` - `{ ... } x := x⁴ - x² - 6 { x ≠ 23 }` - `{ ... } x := (x - 1) · (x + 1) { x ≠ 0}` - `{ ... } X := 1 { X = 10 }` - `{ ... } X := y { X < 0 }` - `{ ... } X := X + y { X > 0 ∧ y > 0 }` - `{ ... } b := b ∧ c { b }` - `{ ... } b := b ∧ c { b => c }` - `{ ... } b := b ∧ c { c => b }` - `{ ... } b := b ∧ c { b = c }` - `{ ... } x, y, z := y, z, X { X = X ∧ y = y ∧ z = z }` - `{ ... } z, y := z · x, y - 1 { y ≠ 0 ∧ z · xʸ = ab }` 2. 给出在以下每种情况下可以替换省略号的最强表达式： - `{ X = 10 } X := X + 1 { ... }` - `{ x² > 45 } X := X + 1 { ... }` - `{ X ≥ 10 } X := X - 10 { ... }` - `{ 0 ≤ X < 10 } X := x² { ... }` - `{ xᵃ = y } x := |x| { ... }` 3. 推导以下语句的最弱前置条件： - `{ ... } y := y + 2x + 1; x := x + 1 { y = x² }` - `{ ... } y := y + 3z + 3x + 1; z := z + 2x + 1; x := x + 1 { y = x³ ∧ z = x² }` - `{ ... } y := y² ; X := X div 2 { yˣ = Z }` - `{ ... } b := b = c; c := b = c; b := b = c { b = B ∧ c = C }` - `{ ... } b := b ≠ c; c := b ≠ c; b := b ≠ c { b = B ∧ c = C }` 4. 找到合适的赋值语句来替换省略号： - `{ z = xʸ ∧ y ≠ 0 } ... ; y := y + 1 { z = xʸ ∧ y > 0 }` - `{ 0 ≤ n < 100 ∧ s = ∑ⁿᵢ₌₁ i³ } ... ; n := n + 1 { 0 < n ≤ 100 ∧ s = ∑ⁿᵢ₌₁ i³ }` - `{ P } x := 2x + 1; ... { P }` 对于所有 `P` 5. 考虑 `{ P } S { Q }` 和 `{ P' } S { Q' }` 的情况，从 Hoare 三元组的解释证明 `{ P ∧ P' } S { Q ∧ Q' }` 和 `{ P ∨ P' } S { Q ∨ Q' }`。 6. 讨论 `abort` 语句的“逆”语句，即对于所有 `P` 由 `{ P } troba { false }` 表征的语句。这种语句在编程语言中是否有用？能否想出一种可能的实现方式？ 7. 找到满足 `{ P } [w ≤ r - q, r := q + 1, r - w | w > r - skip] { q · w + r = x ∧ r ≥ 0 }` 的最弱 `P`。 8. 证明 `{ z · xʸ = Xʸ ∧ y > 0 } [odd(y) - z := z · x | even(y) - skip]; x, y := x², y div 2 { z · xʸ = Xʸ ∧ y ≥ 0 }`。 9. 考虑到守卫的定义良好性，`if` 语句和 `do` 语句的 Hoare 三元组是什么？ 10. 计算满足 `{P ∧ x ≠ y} [b0 -> x := x - y | b1 -> y := y - x] {P}` 的布尔表达式 `b0` 和 `b1`，其中 `P` 由 `x > 0 ∧ y > 0` 给出。 11. 解释以下示例中犯了什么错误： ```plaintext { true } * [true - x := x - 1] { true } inv : true bf : 2x ``` 检查所有证明义务并列出错误的