lab03.dfy：总览
Lab 3(Week 4)注释版。主题三件:用表实现集合、二叉搜索树、停机与 decreases。英文注释是官方题面,原样保留。代码与原件逐字相同,验证结果:21 verified, 0 errors。
前置依赖:hello2 的全部内容——递归函数骨架、手写归纳三件套(match 分案 / 基础空 / 递归调用 = 归纳假设)。本文件在此之上只新增四样东西:类型同义、option、"调用已证引理"、手写 decreases。
基础设施与弹药库
option<V>:要么没有值(None),要么有一个值(Some(v))。它是**"可能查不到"的标准表达**——lookup 找不到键时不能瞎编一个 V 类型的值,就返回 None。比"用 -1 表示失败"干净:类型本身逼你处理两种情况。
◆ type 同义:给 list<int> 起个别名 lset,语义上表示"用表实现的整数集合"。类型层面它就是 list<int>,两个名字完全互通;别名的价值是标注意图。"表实现集合"意味着:允许重复、顺序无所谓——集合语义完全由 member(在不在里面)定义,而不是由表的形状定义。
member 的官方版:用 || 一行写完(hello.dfy 结尾用的是 if-then-else 版,等价)。|| 也短路:x == y 为真就不再递归。
datatype list<T> = Nil | Cons(hd : T, tl : list<T>)
datatype option<V> = None | Some(v : V)
type lset = list<int> // a set of ints, stored as a list
function length<T>(l : list<T>) : nat
{
match l
case Nil => 0
case Cons(_, xs) => 1 + length(xs)
}
function append<T>(l1 : list<T>, l2 : list<T>) : list<T>
{
match l1
case Nil => l2
case Cons(x, xs) => Cons(x, append(xs, l2))
}
function member(x : int, l : list<int>) : bool
{
match l
case Nil => false
case Cons(y, ys) => x == y || member(x, ys)
}弹药库概念:下面两条是已证明、供调用的引理。在后面的证明里写 member_append(a, b, c); 这一句,效果是把它的 ensures 在 (a,b,c) 上的实例注入当前上下文——和调用归纳假设是同一个机制,只是调的是别人不是自己。证明 = 组装已知事实。
◆ <==> 双向箭头:"当且仅当",两个命题互推。member_append 读作:x 在拼接表里 ⟺ x 在 l1 里或在 l2 里。这条是 addexact(本文件最难一题)的钥匙,先记住它长什么样。
lemma lengthAppend<T>(l1 : list<T>, l2 : list<T>)
ensures length(append(l1, l2)) == length(l1) + length(l2)
{}
lemma member_append(x : int, l1 : list<int>, l2 : list<int>)
ensures member(x, append(l1, l2)) <==> member(x, l1) || member(x, l2)
{}Part A：集合操作与特征引理（Ex1–5）
Ex1・insert:头插一个 Cons 完事。x 已在 A 里怎么办?——不管。表里出现两次,member 照样只回答"在",集合语义不受损。这是"表实现集合"换来的便宜。
Ex2・delete——全删(正因为 insert 允许重复,delete 必须删干净,否则 member_delete 那条引理不成立)。骨架依旧:头等于 x 丢掉头、头不等于 x 留下头,两个分支都递归——遍历整张表,一个不漏。
Ex3・anyElement:选择器 A.hd 只有在验证器能证明 A 是 Cons 时才放行——requires A != Nil 正是这份证明的来源。写 requires A.Cons? 完全等价(两个构造子,非 Nil 即 Cons)。hello2 的 zipPartial 讲过:requires 是函数体内可定义性证明的原材料,这里是最小示例。
function insert(x : int, A : lset) : lset
{
Cons(x, A)
}
function delete(x : int, A : lset) : lset
{
match A
case Nil => Nil
case Cons(y, ys) => if x == y then delete(x, ys) else Cons(y, delete(x, ys))
}
function anyElement(A : lset) : int
requires A != Nil
{
A.hd
}Ex4・特征引理这个概念:把"函数对数据做了什么"翻译成"函数对命题做了什么"。insert 改的是表;这条引理说的是它对 member 这个判断的影响——x ∈ insert(y,A) ⟺ x==y ∨ x∈A。题目给了英文句子,工作是逐词译成逻辑:"precisely when" → <==>,"or" → ||。证明不需要归纳:insert 没有递归,展开一层定义即得,{}。
Ex5・delete 的特征引理:"not" → !=,"AND" → &&。delete 是递归的,这里 {} 能过——自动归纳接住了。Part A 至此配平:一对操作各配一条特征引理,集合的行为被完整刻画。
lemma member_insert(x : int, y : int, A : lset)
ensures member(x, insert(y, A)) <==> x == y || member(x, A)
{}
lemma member_delete(x : int, y : int, A : lset)
ensures member(x, delete(y, A)) <==> x != y && member(x, A)
{}Part B：二叉搜索树,定义（Ex6–9）
BST:每个节点存一对(键 k, 值 value),外加左右子树。有序不变量:左子树所有键 < k < 右子树所有键。 注意题面那句括号:有序性是假设的,不检查——lookup 的正确性建立在调用者守约之上。(用 Dafny 把不变量写成谓词并强制检查是可以做到的,超出本 lab 范围。)
◆ 语法细节:字段类型写的是裸 btree,没带 <V>——在自身定义内部,Dafny 默认补全为 btree<V>。
datatype btree<V> = Lf | Node(k : int, value : V, left : btree, right : btree)Ex6・size:与 hello2 的 treeSize 同一个函数,换了构造子名字。Part B 的训练点在于:题面是英文,签名要你自己定——返回"个数",所以是 nat;树的元素类型无关紧要,所以泛型 <V> 照抄进签名。
Ex7・lookup:返回类型 option<V>——找到 → Some(v),没有 → None(option 的用武之地)。三分逻辑直接翻译题面:等于→命中;小于→只进左子树;否则→只进右子树。每层只走一边——这就是"利用有序性高效搜索";如果树不守有序约定,lookup 会漏找,但那是调用者违约,不是 lookup 的错。
Ex8・insertT:◆ Dafny 不允许重载——同一文件里两个函数不能同名,参数类型不同也不行,所以改名 insertT。四种去向,对应四行:Lf 走到空位造新节点;键相等覆盖旧值,子树原样——树的形状一点没变;键更小往左插,右子树原样抄回;否则对称。注意**"函数式更新":不是修改原树,是造一棵新树,没动的部分直接复用。覆盖分支是后面 addcheck 里 ≤ 号的来源。**
Ex9・keylist——中序遍历:左、根、右。题面括号里的提示指的就是 append:"左边的键表,接上(k 打头的右边键表)"——把 k 用 Cons 缝在右表前面,再整体接到左表后面。因为树有序,出来的表恰好升序——但本 lab 不证这一点。
function size<V>(t : btree<V>) : nat
{
match t
case Lf => 0
case Node(k, v, l, r) => 1 + size(l) + size(r)
}
function lookup<V> (key : int, t : btree<V>) : option<V>
{
match t
case Lf => None
case Node(k, v, l, r) =>
if key == k then Some(v)
else if key < k then lookup(key, l)
else lookup(key, r)
}
function insertT<V>(key : int, value : V, tree : btree<V>) : btree<V>
{
match tree
case Lf => Node(key, value, Lf, Lf)
case Node(k, v, l, r) =>
if k == key then Node(key, value, l, r)
else if key < k then Node(k, v, insertT(key, value, l), r)
else Node(k, v, l, insertT(key, value, r))
}
function keylist<V>(tree : btree<V>) : list<int>
{
match tree
case Lf => Nil
case Node(k, v, l, r) => append(keylist(l), Cons(k, keylist(r)))
}Part B：树引理（Ex10–14）
Ex10・lastinsert:"刚插进去的立刻能查到"。lookup 和 insertT 沿同一条键路径下行,自动归纳对得齐,{}。(签名里 tree : btree 又是裸写法,Dafny 补 <V>。)
Ex11・twoinsert:"插入不相干的键,不影响别的查询"。requires key1 != key2 不可省:两键相等时 insertT 会覆盖,等式变假——引理的前置条件划定命题为真的疆界,这和函数的 requires 保证可定义性是同一机制的两种用途。
Ex12・addcheck——为什么是 ≤ 不是 ==:键已存在时走覆盖分支,size 不变。两种情况(+1 或 +0)合起来只能说 ≤。自动归纳过,{}。
lemma lastinsert<V>(key : int, value : V, tree : btree)
ensures lookup(key, insertT(key, value, tree)) == Some(value)
{}
lemma twoinsert<V>(key1 : int, key2 : int, value1 : V, value2 : V, tree : btree<V>)
requires key1 != key2
ensures lookup(key2, insertT(key1, value1, tree)) == lookup(key2, tree)
{}
lemma addcheck<V>(key : int, value : V, tree : btree<V>)
ensures size(insertT(key, value, tree)) <= size(tree) + 1
{}Ex13・addexact——本文件最难一题,拆开看。
命题:键不在树里(!member(key, keylist(tree))),插入后 size 恰好 +1。"不在树里"没有现成谓词,用已有零件拼:member ∘ keylist——Part A 和 Part B 的工具在这里合流。
为什么 {} 不够:归纳到 Node(k,v,l,r) 时,需要把"key 不在整棵树的键表里"拆成"不在左键表、不等于 k、不在右键表"三份,才能喂给子树的归纳假设。而整棵树的键表是 append(左, Cons(k, 右))——拆 append 里的 member,正是弹药库里 member_append 的职责。自动归纳不会主动去调一条外部引理,只能你来。
证明逐行:match 老三件套开场,Lf 分支空(插进空树,size 0→1,定义展开即得);member_append(...) 注入分解事实——结合 requires,当前上下文立得 key ∉ 左键表、key != k、key ∉ 右键表;if key < k:insertT 走左边,右子树原封没动——调用左边的归纳假设,得左边 size 恰 +1,全树随之 +1;else if key > k:对称;else 呢?没写。 key == k 的分支落空——但上一步已推出 key != k,这个分支不可达:前提自相矛盾的分支里任何验证义务自动成立。(hello2 的 zipPartialLength 见过一次,这里是主动利用它省掉一个分支。)
lemma addexact<V>(key : int, value : V, tree : btree<V>)
requires !member(key, keylist(tree))
ensures size(insertT(key, value, tree)) == size(tree) + 1
{
match tree
case Lf =>
case Node(k, v, l, r) =>
member_append(key, keylist(l), Cons(k, keylist(r)));
if key < k {
addexact(key, value, l);
} else if key > k {
addexact(key, value, r);
}
}Ex14・keysLength:键的个数 == 节点数。手写的原因同上:目标里出现 length(append(...)),需要 lengthAppend 来把它换成两段长度之和——外部引理,必须点名调用。配方 = 树归纳双假设 + 一条外部引理。三行注入后账目:length(键表) = length(左键) + 1 + length(右键) = size(l) + 1 + size(r) = size(t),SMT 收尾。记住这个组合拳:归纳假设 + 弹药库,lab04 的 Part V 还是它。
lemma keysLength<V>(t : btree<V>)
ensures length(keylist(t)) == size(t)
{
match t
case Lf =>
case Node(k, v, l, r) =>
keysLength(l);
keysLength(r);
lengthAppend(keylist(l), Cons(k, keylist(r)));
}Part C：停机与 decreases（Ex15–16）
停机的完整规则,一次讲清。 到目前为止所有递归都是结构递归——递归调用作用在参数的组成部分上(xs 之于 l,子树之于树,n-1 之于 nat n),Dafny 免检放行。本节的递归不是:lo 往上数,参数在变大。Dafny 需要你指一个真正在变小的量——decreases 子句。把它当成递归门口的量具:每次进门前后各量一次,验证器检查两件事——①严格变小;②不会掉到 0 以下(有底,不能无限跌)。两条都满足,下降必然止步,停机得证。
Ex15・upList:变小的量是差距 hi - lo——lo 每进一步,差距缩一格;requires lo <= hi 保证差距 ≥ 0(②的底)。产出 [lo, lo+1, ..., hi-1],注意右端开——lo == hi 时给 Nil。
function upList(lo : int, hi : int) : list<int>
requires lo <= hi
decreases hi - lo
{
if lo == hi then Nil else Cons(lo, upList(lo + 1, hi))
}Ex16・fib_loop——题面那句 WHY IS THIS??? 的完整回答:
fib_loop 靠 i 一路 +1 追上 n 来停。若一开始 i > n,i 只会越追越远,n == i 永远不成立——这个函数本来就不对所有输入停机。所以任何 decreases 都单独救不了它:对 i > n 的输入,根本不存在下降的量。
出路:requires i <= n 把危险输入拦在门外。契约之内,n - i 就是合法量具(≥ 0 有底、每次递归 −1 严格变小)。接着验证器检查每个调用点守约:fib 体内,n == 0 已被 if 截走,进到 else 时 n ≥ 1,传入 (1, 0, 1, n),1 <= n ✓;递归点,走到 else 说明 n != i,叠加已知 i <= n,得 i < n,故 i + 1 <= n ✓。一个"部分停机"的函数,被 requires 收编成契约内全停机——requires 与 decreases 在停机证明里是搭档,不是两个孤立知识点。
顺带看懂算法本身:fi、fpi 是相邻两个 Fibonacci 数,每步 (fi, fpi) ← (fi + fpi, fi) 滚动前进——线性时间,对比朴素双递归的指数时间。
/* fi = i'th fib number; fpi = fib number of i - 1 ("previous to i") */
function fib_loop(fi : nat, fpi : nat, i : nat, n : nat) : nat
requires i <= n
decreases n - i
{
if n == i then fi
else fib_loop (fi + fpi, fi, i + 1, n)
}
function fib(n:nat) : nat
{
if n == 0 then 0
else fib_loop(1,0,1,n)
}