lab04-SOLUTION.dfy：总览
Lab 4(Week 5)官方答案注释版。六个部分:日期、requires、列表编程、停机、难证明、量词。前三个 lab 的所有工具在这里汇合,并新增最后一块拼图:量词(forall / exists)与见证(witness)。
★ 重要:官方答案里 Q16 的 subset_antisym 在 Dafny 4.11.0 下验证不通过(缺了一个方向)。本文给出修正版,官方原文保留在该处,差异讲清。除这一处外,代码与官方逐字相同。全文验证结果:30 verified, 0 errors。
Part I：日期（Q1–Q6）
Q1・daysInMonth——月份建模,第二方案。 hello.dfy 用的是 datatype month(十二个构造子);这里用裸 nat 加 requires 0 <= m <= 11——注意:0 起数,0 是一月,11 是十二月。这个约定贯穿整个 Part I,Q5 有个陷阱专等忘记它的人。
两种建模的代价对比:datatype——非法月份在类型层面不存在,match 穷尽性免费;代价是和数字互转要自己写。nat + requires——算术方便(Q3 的 m-1 递归全靠它);代价是每个函数都得背上 requires。
◆ 语法点:对 nat 做 match,列出 0..11 十二个字面量,没有 case _ 默认分支——为什么穷尽性检查能过?因为 requires 排除了其余取值,剩下的分支不可达,Dafny 确认后放行。lab03 的 addexact 里"不可达分支可省"在 match 穷尽性上的翻版。删掉 requires,这里立刻报 missing case。
2 月写成 28 + (if isLeapYear then 1 else 0):if 表达式嵌在算式里当一个数用。参数 isLeapYear 是个 bool 形参,恰好和 Q2 的谓词同名——两个不同的东西,作用域内以近者为准,读代码时留意。
function daysInMonth(m : nat, isLeapYear : bool) : nat
requires 0 <= m <= 11
{
match m
case 0 => 31 case 1 => 28 + (if isLeapYear then 1 else 0)
case 2 => 31 case 3 => 30 case 4 => 31 case 5 => 30
case 6 => 31 case 7 => 31 case 8 => 30
case 9 => 31 case 10 => 30 case 11 => 31
}输出范围引理:任何合法月份的天数都在 [28, 31] 里。ensures 里也能链式比较。引理自带 requires——引用它之前得先满足前置,和函数一个规矩。(另一种设计是把这条 ensures 直接写在 daysInMonth 上,所有调用点免费获得;写成独立引理则需要时手动调。两种放置法都合法,权衡是"污染签名"对"调用时点名"。)
lemma daysInMonthOutputOK(m:nat, isLeapYear:bool)
requires 0 <= m <= 11
ensures 28 <= daysInMonth(m,isLeapYear) <= 31 {}Q2・isLeapYear——闰年,纯逻辑一行版。 对照 hello.dfy 的 if 链版本——等价,但这版是题面的直译:"divisible by 4, and" → y % 4 == 0 &&;"when P, also Q" → (P ==> Q)。
◆ ==> 是蕴含:"如果左边真,则右边真;左边假时整体自动真"。P 假时蕴含为真这一点(空真)是逻辑新手的第一道坎:年份不被 100 整除时,括号整体为真,闰不闰全看 % 4。
◆ 括号不可省:&& 比 ==> 结合得紧,去掉括号会被解析成 (y%4==0 && y%100==0) ==> y%400==0——一条完全不同且错误的命题(它对 y=2023 也为真!)。运算符优先级从松到紧:<==>,==>,||,&&,比较,算术。写逻辑式,拿不准就加括号。
predicate isLeapYear(y : nat)
{
y % 4 == 0 && (y % 100 == 0 ==> y % 400 == 0)
}Q3・daysUpToStartOf——递归前缀和。"m 月之前的天数 = (m-1) 月之前的天数 + (m-1) 月自身的天数",基础情况 0 月之前是 0 天。数字上的递归和列表上的递归是同一个思路——把问题推给更小的输入。
两处验证器在暗中工作:case _ 分支里 Dafny 记得 m != 0,所以 m - 1 : nat 合法;调用 daysInMonth(m-1, ...) 要过它的 requires——由 m <= 11 且 m >= 1 推得 0 <= m-1 <= 10。停机:m 每次减一的 nat,免检。
function daysUpToStartOf (m:nat, isLeapYear : bool) : nat
requires 0 <= m <= 11
{
match m
case 0 => 0
case _ => daysUpToStartOf(m-1,isLeapYear) + daysInMonth(m-1,isLeapYear)
}
// 测试引理，标准形态：命题进 ensures，体留空 {}。
lemma dAprilTrue()
ensures daysUpToStartOf(3, true) == 91 {}Q4・date_lt——单构造子 datatype 与字典序。 date 只有一种造法 D(日, 月)——用 datatype 给一对数起名字、贴标签,比裸元组多一层意图表达。
◆ 字典序(lexicographic order):先比主关键字(月),月相同再比次关键字(日)。直译成逻辑:月更小 ∨ (月相同 ∧ 日更小)。这个结构值得多看一眼——lecture 7 里多参数递归的 decreases (a, b) 词典序度量,数学骨架与此完全相同:高位严格降,或高位持平低位降。
datatype date = D (day : nat, month : nat)
predicate date_lt(d1 : date, d2 : date)
{
d1.month < d2.month || (d1.month == d2.month && d1.day < d2.day)
}Q5・★陷阱题:月份 0 起数! 十月是 9,十二月是 11——D(12, 9) 是"10 月 12 日"。写成 D(12, 10) 照样能验证通过(11 月 12 日也早于 D(2, 11)),但证的不是题目那句话。验证器只管写下的命题真不真,不管它是不是你想说的——形式化这一步没人替你把关。
lemma twelveOct_lt_twoDec()
ensures date_lt(D(12,9), D(2,11)) {}Q6・三分律(trichotomous)。 任意两个日期,要么 <,要么 ==,要么 >。"either ... or"(三选一)→ 三个命题用 || 连。◆ datatype 的 == 是结构相等:日和月分别相等。{} 通过:无递归无归纳,纯粹的整数三分律,SMT 的本行。
lemma date_lt_trichotomy(d1:date, d2:date)
ensures date_lt(d1,d2) || d1 == d2 || date_lt(d2,d1) {}Part II：requires（Q7–Q8）
老朋友们的紧凑排版(内容与前几个文件一字不差),加两个新角色:
◆ subset(l1, l2):l1 的每个元素都是 l2 的成员。读它的递归:空表是任何表的子集(空真!没有元素可违规);Cons(x, xs) 是 l2 的子集 ⟺ x ∈ l2 且 xs ⊆ l2。一条 && 链把"所有元素都在"铺开。
◆ subset_member:本文件 Part V 的弹药——x ∈ A 且 A ⊆ B,则 x ∈ B。"子集"这个批发承诺在单个元素 x 上的零售兑现。 语法点:requires 可以写多条(也可用 && 合成一条),全部满足才算守约。
datatype list<T> = Nil | Cons(hd:T, tl: list<T>)
type ilist = list<int>
predicate member(i : int, l : ilist) {
match l case Nil => false case Cons(h,t) => i == h || member(i,t)
}
function length<T>(l : list<T>) : nat {
match l case Nil => 0 case Cons(_, t) => 1 + length(t)
}
function append<T>(l1 : list<T>, l2:list<T>) : list<T> {
match l1 case Nil => l2 case Cons(h,t) => Cons(h,append(t,l2))
}
predicate subset(l1 : ilist, l2 : ilist) {
match l1 case Nil => true
case Cons(x,xs) => member(x,l2) && subset(xs,l2)
}
lemma subset_member(x:int, A:ilist, B:ilist)
requires member(x,A) requires subset(A,B)
ensures member(x,B) {}Q7・div12——requires 的顺序性,全课程最干净的示范。 三条前置从上到下读,每一条都站在前面所有条的肩膀上:
requires l.Cons? l 非空 —— 此后 l.hd、l.tl 合法
requires l.tl.Cons? 尾也非空 —— 写这条时用到了 l.tl，它的合法性来自上一条！
requires l.tl.hd != 0 第二个元素非零 —— 为除法护航把第二条挪到第一条前面试试:l.tl 立刻被拒——requires 自己也要"有定义",其可用前提是排在它之前的条款。这与 hello.dfy 里 && 短路保护 m % n 是同一个原理,从表达式层面升级到了契约层面。(题面 HINT 的另一路:requires match l case Cons(_, tl) => ...——match 也能出现在 requires 的命题里。风格自选。)
function div12(l : ilist) : int
requires l.Cons? requires l.tl.Cons? requires l.tl.hd != 0
{
l.hd / l.tl.hd
}Q8・测试引理顺带揭示两件事:14 / 6 == 2——整数除法向下取整(hello.dfy 的 gradient 埋过这颗雷);第三个元素 3 完全无关——div12 只碰前两个。测试用例挑得好,能把函数的语义边界照出来。
lemma testing_div12()
ensures div12(Cons(14,Cons(6,Cons(3,Nil)))) == 2 {}Part III：列表编程（Q9–Q12）
Q9・interleave——交错。 嵌套 match 分三案:l1 空 → 剩下的全是 l2,整个返回("长表余下接尾");l1 非空但 l2 空 → 对称,返回 l1;都非空 → 各取一头,x 在前 y 在后("starting with the first element of the first list"),压两层 Cons,余下递归。递归时两表各短一截——同步下降。
◆ 设计决策:这里不 requires 等长。 题面明说允许不等长;而且加了多余前置会立刻殃及下游——Q10 的测试、Q11/Q12 的引理全得跟着背上同样的前置。前置条件是债,能不借就不借。
function interleave<T>(l1 : list<T>, l2 : list<T>) : list<T>
{
match l1
case Nil => l2
case Cons(x,xs) =>
match l2
case Nil => l1
case Cons(y,ys) => Cons(x,Cons(y,interleave(xs,ys)))
}Q10・测试引理。 把 Haskell 记号 [1,2,3] 手工展开成 Cons 链——枯燥,但这就是本课程的表字面量。
lemma testInterleave()
ensures interleave(Cons(1,Cons(2,Cons(3,Nil))), Cons(4,Cons(5,Cons(6,Nil)))) ==
Cons(1,Cons(4,Cons(2,Cons(5,Cons(3, Cons(6,Nil)))))) {}Q11・length_interleave——{} 直接过,值得停一秒。 interleave 是双表同步递归、三分支,花哨程度远超 append,自动归纳照样接住。自动归纳的成败不看代码复杂度,看目标命题与递归结构对不对得齐——这条引理的归纳恰好沿着 interleave 自己的递归轨道走。
lemma length_interleave<T>(l1:list<T>, l2:list<T>)
ensures length(interleave(l1,l2)) == length(l1) + length(l2) {}Q12・member_interleave1。"l1 的成员必是交错结果的成员"。注意这条用 requires/ensures 表达蕴含(守约者视角),而不是 ensures member(...) ==> member(...)(命题视角)——两种写法这里都行,requires 版调用起来更顺手。{} 过。
lemma member_interleave1(i : int, l1: ilist, l2:ilist)
requires member(i,l1)
ensures member(i, interleave(l1,l2)) {}Part IV：停机（Q13–Q14）
Q13・upToNList——与 lab03 的 upList 一字不差(课程连出两遍,掂量一下分量):向上数 → 差距 end - start 在缩 → decreases 之;requires start <= end 给差距垫底(≥ 0)。
function upToNList(start: int, end : int) : ilist
requires start <= end decreases end - start
{
if start == end then Nil
else Cons(start, upToNList(start + 1, end))
}Q14・◆ 引理上也挂了 decreases——第一次见,值得较真。
实测(Dafny 4.11.0):删掉这条 decreases,验证失败。原因:{} 依赖自动归纳,而归纳需要一个"什么在变小"的良基度量。此前的引理参数是 nat 或 datatype,自带结构度量;这里参数是两个 int——int 本身没有底,自动归纳无从下脚。decreases end - start 就是递给归纳引擎的度量:告诉它沿这个量做归纳。函数要停机凭据,归纳要下降凭据——同一枚硬币的两面,同一个子句伺候。
lemma length_upToNList(start : int, end : int)
requires start <= end
decreases end - start
ensures length(upToNList(start,end)) == end - start
{}Part V：难证明（Q15–Q16）
Q15・subset_transitive——这条证明是半自动的,看懂它等于看懂 Dafny 证明的分工。
实测:{} 空体失败——所以确实需要人出手。但官方体里没有递归调用 subset_transitive(arest,B,C),却过了。谁补上了尾巴 arest 的归纳假设?——自动归纳。 Dafny 对 lemma 默认尝试注入归纳假设,即使体非空。这里人只需补机器缺的那一块:头元素 a 的去向。目标展开后要 member(a, C),而已知只有 member(a, B)(subset(A,B) 的 Cons 分支)与 subset(B,C)——搭桥的正是弹药 subset_member。调用一句,头的账清了,尾的账自动归纳清,合拢。
lemma subset_transitive(A : ilist, B : ilist, C : ilist)
requires subset(A,B) requires subset(B,C) ensures subset(A,C)
{
match A
case Nil => {}
case Cons(a,arest) => subset_member(a,B,C);
}◆ 全手动版同样通过,且考试时更稳妥(不赌启发式):
match A
case Nil => {}
case Cons(a,arest) => {
subset_member(a,B,C);
subset_transitive(arest,B,C);
}多写一行归纳假设调用,万无一失。语法点:case Nil => {} 里的 {} 是空语句块,与 case Nil => 后面直接空着等价。
Q16・★ 官方答案在此验证失败。 官方原文是:
lemma subset_antisym(i : int, A : ilist, B : ilist)
requires subset(A,B) requires subset(B,A)
ensures member(i,A) <==> member(i,B)
{
if member(i,A) { subset_member(i,A,B); subset_member(i,B,A); }
}Dafny 4.11.0 报错:a postcondition could not be proved。诊断:<==> 是两个方向的合同。
- ⟹ 方向(i∈A 则 i∈B):if 分支里第一句 subset_member(i,A,B) 已经搞定;第二句 subset_member(i,B,A) 推回 member(i,A)——本来就已知,纯属空转。
- ⟸ 方向(i∈B 则 i∈A):需要在 member(i,B) 成立的前提下调 subset_member(i,B,A)。但官方的 if 守的是 member(i,A):当 i∈B 而 i∉A 时(正是要排除的反例场景),if 不进,什么也没发生——这个方向无人认领,验证器如实拒收。
修正:两个方向各立一个 if,结构对称,各调各的桥。顺带学到 if 语句可以没有 else,以及一课:官方答案也要过验证器这一关——机器不认作者。
lemma subset_antisym(i : int, A : ilist, B : ilist)
requires subset(A,B) requires subset(B,A)
ensures member(i,A) <==> member(i,B)
{
if member(i,A) { subset_member(i,A,B); }
if member(i,B) { subset_member(i,B,A); }
}Part VI：量词（Q17–Q18）
Q17・nth——requires n < length(l) 一石三鸟:
- l 是 Nil 时 length 为 0,而 nat 的 n < 0 无解——Nil 情形被前置条件整个排除,所以 match 里只写 Cons 一个 case 也算穷尽(不可达分支干脆不写,比 lab03 addexact 的空 else 更进一步);
- 递归调用 nth(n-1, t) 要过自己的前置:n ≥ 1(else 分支)且 n < length(l) = 1 + length(t) ⟹ n-1 < length(t);
- n ≥ 1 保证 n-1 仍是 nat。
一条前置,三处验证义务同时清账。
function nth<T>(n : nat, l : list<T>) : T
requires n < length(l)
{
match l
case Cons(h,t) => if n==0 then h else nth(n-1,t)
}Q18・member_nth——全套 lab 的收官之作,量词登场。
◆ exists 语法:exists n : nat | n < length(l) :: nth(n,l) == i,读作"存在自然数 n,满足 n < length(l),使得 nth(n,l)==i"。| 后面是对 n 的范围限定,:: 后面是主体命题。整句等价于 exists n : nat :: n < length(l) && nth(n,l) == i,竖线只是把"资格条件"和"真正要说的话"分开写,更清晰。
◆ 证明一个 exists(引入):拿出一个具体的见证 witness。使用一个 exists(消去):从"存在"里取出那个见证来用,语法是"选取赋值" :|——var n0 : nat :| 条件; 读作"取一个满足条件的 n0"。前提:验证器必须已经知道这样的 n0 存在(某个 exists 已在上下文中成立),否则拒绝。
ensures 是 <==>,两个方向:⟸(存在下标 ⟹ 是成员)验证器自动搞定(沿 nth 的递归即可),体内一字未提。⟹(是成员 ⟹ 存在下标)手工施工——match 只写 Cons(member(i, Nil) 为 false,if 根本进不来,Nil 分支不可达,又一次),再分两情形:
- i == j:成员就是头,下标 0 就是见证。assert nth(0,l) == i 亮出具体见证,验证器由此自行概括出 exists(这一句就是存在性引入)。
- i != j:成员藏在尾 js 里。assert member(i,js) 由定义展开得到,这一步同时触发归纳假设——本引理在 js 上的实例(自动归纳注入)给出"js 上的 exists 成立"。存在性消去:
var n0:nat :|把 js 里那个见证下标取出来。换算回整表:js 的第 n0 个 = l 的第 n0+1 个(nth 的定义顺推一步);新见证的资格条件也要备齐(n0+1 < length(l));最后存在性引入,n0+1 就是 l 上的见证,合拢。
一进一出(:| 取证、assert 交证),exists 的用法全在这一段里。
lemma member_nth(i:int, l : list<int>)
ensures member(i, l) <==> exists n : nat | n < length(l) :: nth(n,l) == i
{
if member(i,l) {
match l
case Cons(j,js) => {
if i == j {
assert nth(0,l) == i;
} else {
assert member(i,js);
var n0:nat :| n0 < length(js) && nth(n0,js) == i;
assert nth(n0 + 1, l) == i;
assert n0 + 1 < length(l);
assert exists n : nat | n < length(l) :: nth(n,l) == i;
}
}
}
}