递归的终止性
0! = 1 —— 数学定义上空乘积为 1。
基例(base case):递归函数里不调用自己、直接给出答案的那个分支。与之相对,调用自己的分支叫递归步。
递归的本质是"把问题踢给一个更小的自己",不能无限踢皮球。
参数用 nat 不是随手写的,验证器要证明递归会停。递归不是白拿的,你得让 Dafny 相信它会终止。
bad1 —— 没有基例
function bad1(m: nat): nat { m * bad1(m) }bad1(3) = 3 · bad1(3) = 3 · 3 · bad1(3) …
没有 if,没有出口,调用自己时参数原封不动,永远到不了底。
bad2 —— 方向反了
function bad2(m: nat): nat { if m == 0 then 1 else bad2(m + 1) }bad2(3) → bad2(4) → bad2(5) → …
出口在 0,却往正无穷跑,永远够不着。
有基例 m == 0,但递归参数在变大。有基例不代表能到达基例,方向必须朝着基例去。
bad3 —— 从底下漏出去
注意它的类型是 int:
function bad3(i: int): int { if i == 0 then 1 else bad3(i - 1) }bad3(5) → 4 → 3 → … → 0,停了bad3(-1) → -2 → -3 → …——int没有底
这叫 falling off the bottom,从底部掉出去。
nat 有地板(0),减到底就到 0,验证器能证明"每次严格变小 + 有下界 = 必然终止"。
nat是终止性证明的原材料。
三件要素
递归要停,需要:
① 有出口(数学上叫良基关系)：bad1
② 朝出口走：bad2
③ 脚下有底：bad3
off-by-one
function f(n: nat): nat { if n == 100 then 0 else f(n + 1) }应改为 if n >= 100 而不是 if n > 100 —— 边界差一(off-by-one)会 bug。
蕴含 ==>
lemma simple(x: int, y: int)
ensures x < 10 + y ==> 2 * x - 2 * y < 20
{}// scary implication
蕴含有 vacuous truth,验证器对这些情况看都不看。验证器背后的 SMT 求解器(叫 Z3)对这种线性算术是全自动的。
以下两种写法几乎可以互换:
ensures A ==> B
requires A ensures B为什么不写成 if-then-else?
lemma simple(x: int, y: int)
ensures if x < 10 + y then 2 * x - 2 * y < 20 // ✗
{}==> 和 if-then-else 的区别在于层级不同。
一、类型
==> 产 bool,if-then-else 产任何类型。
p ==> q:两侧必须是 bool,结果是 bool。它是和 &&、|| 平级的布尔运算符,在同一个真值表里。
if c then a else b:c 是 bool,但 a、b 可以是任何类型,int、date、point、bool 都行。整个表达式的类型就是分支的类型。
它是分支选择器,不是逻辑算子。所以如果表达式要产非 bool 的值,==> 没有资格出场。
二、else
==> 自带"缺省放行",if 必须两头交代。
p ==> q:没有 else,也不需要。p 假时整体自动 true —— 这就是 vacuous truth。它天生是"单边承诺",只对 p 成立的世界表态,p 不成立的世界一律免责放行。
if c then a else b:else 不可省。表达式必须有值,c 为假时值从哪来,必须交代。
三、语义地位
==> 是"断言的连接词",if 是"计算的岔路"。
看它们各自的主场:==> 活在规约层 —— ensures、lemma、真值表里,那里在陈述事实;if-then-else 活在计算层,那里在产出值。
在两侧都是 bool 时:
p ==> q ≡ !p || q ≡ if p then q else true蕴含 = 一个 else 被钉死为 true 的 if。
所以 ==> 是 if 的一个特例(仅 bool,else 被焊死为 true),if 是 ==> 的泛化。
一句话判断:要值,用
if;要理,用==>。