编辑“︁Lean程序规范”︁

{{DISPLAYTITLE:Lean程序规范}}

'''Lean程序规范'''是[[Lean定理证明器]]中用于形式化描述程序行为的关键工具。它通过数学逻辑精确定义程序应满足的性质，为后续的验证提供严格依据。本文将系统介绍Lean程序规范的基本概念、语法结构、实际应用及验证方法。

== 概述 ==
在Lean中，'''程序规范'''（Program Specification）是程序正确性的形式化描述，通常由以下部分组成：
* '''前置条件'''（Precondition）：程序执行前必须满足的条件
* '''后置条件'''（Postcondition）：程序执行后必须满足的条件
* '''不变式'''（Invariant）：循环或递归过程中保持不变的属性

数学上可表示为霍尔三元组（Hoare Triple）：
<math>\{P\}\ \text{prog}\ \{Q\}</math>
其中：
* <math>P</math> 是前置条件
* <math>\text{prog}</math> 是程序代码
* <math>Q</math> 是后置条件

== 基本语法 ==
Lean使用'''命题即类型'''（Propositions as Types）范式表示规范。以下是典型规范声明：

<syntaxhighlight lang="lean">
-- 函数类型签名与规范结合
def factorial (n : Nat) : Nat :=
  -- 实现部分
  match n with
  | 0 => 1
  | n' + 1 => (n' + 1) * factorial n'
-- 后置条件规范
theorem factorial_spec (n : Nat) : factorial n = Nat.fact n := by
  induction n <;> simp [factorial, *]
</syntaxhighlight>

=== 规范组件详解 ===
{| class="wikitable"
|+ Lean规范关键组件
! 组件 !! 语法示例 !! 描述

| 前置条件 || <code>require h : n ≥ 0</code> || 输入约束

| 后置条件 || <code>ensure result = 2 * x</code> || 输出约束

| 循环不变式 || <code>invariant sum = ∑ i in 0..k, a[i]</code> || 循环保持性质
|}

== 实际案例 ==
=== 案例1：数组求和验证 ===
验证一个数组求和函数的正确性：

<syntaxhighlight lang="lean">
def arraySum (a : Array Nat) : Nat :=
  let rec sum (i : Nat) (acc : Nat) : Nat :=
    if h : i < a.size then
      sum (i + 1) (acc + a[i])
    else
      acc
  sum 0 0

-- 规范表述
theorem arraySum_correct (a : Array Nat) :
  arraySum a = ∑ i in Finset.range a.size, a[i] := by
  sorry  -- 验证证明在此处展开
</syntaxhighlight>

=== 案例2：二分查找规范 ===
<mermaid>
graph TD
  A[Precondition: 有序数组] --> B[Initialize low/high]
  B --> C{low ≤ high?}
  C -->|Yes| D[计算mid]
  D --> E{比较目标值}
  E -->|等于| F[返回mid]
  E -->|小于| G[调整high]
  E -->|大于| H[调整low]
  G & H --> C
  C -->|No| I[返回未找到]
</mermaid>

对应Lean规范：
<syntaxhighlight lang="lean">
def binarySearch (arr : Array α) (target : α) [Ord α] : Option Nat :=
  let rec search (low high : Nat) : Option Nat :=
    if h : low ≤ high then
      let mid := (low + high) / 2
      match compare target arr[mid] with
      | .eq => some mid
      | .lt => search low (mid - 1)
      | .gt => search (mid + 1) high
    else
      none
  search 0 (arr.size - 1)

-- 规范包括：
-- 1. 若返回some i，则arr[i] = target
-- 2. 若返回none，则target ∉ arr
</syntaxhighlight>

== 高级主题 ==
=== 依赖类型规范 ===
对于更复杂的规范，可以使用依赖类型：

<syntaxhighlight lang="lean">
def sortedInsert [Ord α] (arr : Array α) (i : Fin arr.size) (val : α) :
  { out : Array α // out.size = arr.size + 1 ∧ isSorted out } :=
  -- 实现插入操作并返回证明
</syntaxhighlight>

=== 规范组合 ===
通过'''monad'''组合规范（如`StateT`和`ExceptT`）：
<math>\text{Spec} = \text{Pre} \rightarrow \text{Post} \times \text{Invariants}</math>

== 验证技术 ==
Lean提供多种验证规范的方法：
1. '''战术证明'''（Tactic Proofs）
2. '''项风格证明'''（Term Style Proofs）
3. '''SMT求解'''（通过`lean_smt`）

示例验证策略：
<syntaxhighlight lang="lean">
example (x : Nat) : x + 1 > x := by
  apply Nat.lt_succ_self  -- 使用标准库引理
</syntaxhighlight>

== 最佳实践 ==
* 保持规范与实现分离
* 优先使用可组合的规范
* 为关键循环和递归函数添加不变式
* 使用`have`语句分解复杂规范

== 常见错误 ==
{| class="wikitable"
|+ 规范编写常见问题
! 错误类型 !! 示例 !! 修正方案

| 过于宽松 || <code>ensure result ≥ 0</code> || 添加精确约束

| 遗漏边界条件 || 忽略空输入 || 添加<code>a.size > 0</code>

| 循环不变式过弱 || 仅保持部分性质 || 包含全部必要状态
|}

== 总结 ==
Lean程序规范是形式化验证的基石，通过：
* 数学精确的描述语言
* 与实现紧密集成的语法
* 丰富的验证工具链
使开发者能构建高可靠性的软件系统。初学者应从简单函数规范开始，逐步掌握依赖类型等高级特性。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean程序验证]]