8.15 辛酉
building-intlists.dfy
datatype intlist = Empty | Cons(hd: int, tl: intlist)
function singleton(i: int): intlist
// what "ensures line" might we write here?
{
Cons(i, Empty)
}
// what more interesting functions might we write to build lists?
// - of different lengths
// - with successive elements
// - ?-
为什么写成 datatype intlist = Empty | Cons(hd: int, tl: intlist)
-
singleton 是什么意思?
-
selector 是什么, singleton(i).hd 吗?
-
我笔误写成了：
datatype intlist = Empty | Cons(hd: list, tl: intlist)
应该是 int ↑
↑ 剩下的整条列表
单个整数一条 intlist, 要么是 Empty(空, 到此为止), 或者是 Cons, 一个整数头, 一条 intlist 尾。
第一个坑装乘客(int), 第二个坑装车厢(intlist 自己), 套娃的自引用只发生在第二个坑。
它和 list<T> 的关系: 这是焊死了元素类型的简装版。Nil 改名为 Empty, 名字自由。
- singleton 本义是"单元素的"。这个函数干的事: 收一个整数, 吐一条只装着它的列表。
singleton(7) 得到 [7], 即 Cons(7, Empty)
这是全课程第一个"造列表的函数"。它的价值只在示范函数的最小形态。
- selector 选择器是从造好的值里取某个坑的内容: ".坑名", 坑名来自 datatype 声明。
第一行写了 hd 和 tl, 于是任何一个 Cons 造的值都能 .hd 取头, .tl 取尾。
singleton(i) = Cons(i, Empty)
singleton(i).hd = i
singleton(i).tl = Empty
①match: 不知道是哪种情况, 分案讨论
②selector: 明知道是 Cons, 直接伸手拿。伸手的前提是：不是 Empty, Empty 括号里一个坑都没
selector 的真正用武之地不在函数体里, 而在规格语言里描述"结果长什么样"
building-intlists.dfy
datatype intlist = Empty | Cons(hd: int, tl: intlist)
function singleton(i: int): intlist
// what "ensures line" might we write here?
{
Cons(i, Empty)
}
// what more interesting functions might we write to build lists?
// - of different lengths
// - with successive elements
// - ?给它写条什么样的 ensures?
ensures singleton(i) != Empty
ensures singleton(i).hd == i // selector 派上用场了
ensures singleton(i).tl == Empty
ensures singleton(i) == Cons(i, Empty) 规格 Spec 该写多强?singleton 造的列表长度焊死是1, 注释问: 怎么造长度可变, 元素连续的列表?
递归转向 —— 递归地消耗一个数字, 产出一条列表。
function countdown(n: nat): intlist
{
if n == 0 then Empty
else Cons(n, countdown(n-1))
}countdown(3) 展开: Cons(3, countdown(2)) → Cons(3, Cons(2, countdown(1))) → 最终 [3,2,1]。递归终点是0(产出 Empty)。n 传多大, 列表就多长, 元素还是连着的
如果参数类型不是 nat 是 int, 那传负数进去, n-1 离0越来越远, 递归不终止
Dafny 对每个递归函数都要证明它会停。
intlist.dfy
datatype intlist = Empty
| Cons(hd: int, tl: intlist) .字段名
// write some variations on this with selectors ".fldname" and
// pattern-matching to get particular output numbers
function dumb(): int
ensures dumb() == 0
{
var l := Cons(0, Cons(1, Cons(2, Empty))); l是列表 [0,1,2]
l.hd l.hd 就是 0
} l.tl 是 [1,2]
l.tl.hd 是 1
l.tl.tl.hd 是 2selector 和 match 用哪个?
l.hd 有个前提: l 得真的是 Cons, 如果 l 是 Empty, 验证器会在编译时拦下来。
①match: 不知道手里是哪种情况时用, 要把每种情况都处理掉
②selector: 已经确定(且能让验证器信服)是哪个构造子时用。
l.tl.tl.tl 是 Empty, l.tl.tl.tl.hd 会被验证器拦
list-maximum.dfy
datatype list<T> = Nil | Cons(hd: T, tl: list<T>)
function maxList(l: list<int>): int
// with an accumulatorlist: 我们起的类型名。
<T> 是说这个类型带一个空位。T 是个占位符。
list<T> 读作: "list 是一族类型的模版, 装什么由你定"
Nil 是空列表吗?
Nil 是一个不带任何数据的值。代表"什么元素都没有的列表"。
同一个东西有 Empty, Lf。作用是给递归一个终点。
| 是什么?
读作"或者"。整个第一行连起来读: "一个 list 类型的值, 要么是 Nil, 或者是 Cons(某个头, 某条尾巴)"
| 隔开的每一项叫一个构造子。造这个类型的值只有这几种办法, 没有第三种
这也是为什么 match 写两个 case 就齐了。| 隔开几次, match 就要写几个 case
点菜只能从菜单里选。
同一行里所有的 T 只能填一个东西。
function 函数名(参数名: 参数类型): 返回值类型。
"maxList 这个函数, 吃一个整数列表(给它起名 l), 吐一个整数"
requires length(l) > 0 整条列表的最大值 = 头 和剩余部分的最大值 两者取大
{
match l
case Cons(hd, Nil) => hd // 恰好一个元素
case Cons(hd, tl) => max(hd, maxList(tl))
}
↑
function max(i: int, j: int): int 这里 recursive 了吧?
{ if i < j then j else i }case Cons(hd, tl) ⇒ max(hd, maxList(tl)) ✗
递归maxList(tl)也带着 requires length > 0 的合同。可 tl 可能是空的。(列表只剩一个元素)
accumulator 版:
function maxListA(l: list<int>, maxSoFar: int): int
{
match l
case Nil => maxSoFar
case Cons(hd, tl) =>
var newMaxSoFar := max(hd, maxSoFar);
maxListA(tl, newMaxSoFar)
}
function maxListWithA(l: list<int>): int
requires length(l) > 0
{
match l
case Cons(hd, tl) => maxListA(tl, hd)
}maxListWithA([2,7,4])
= maxListA([7,4], 2)
= maxListA([4], max(7,2))
= maxListA([4], 7)
= maxListA([Nil], max(4,7)) //不能写成[Nil]，Nil 就是空列表, 不需要套 []
= maxListA([Nil], 7) // = maxListA(Nil, 7)
= 7 写递归函数, 先 match 搭骨架
maxList[2,7,4]
= max(2, maxList[7,4])
= max(2, max(7, maxList[4]))
= max(2, max(7, max(4))) //Cons(hd, Nil) ⇒ hd 直接得4
= max(2, max(7,4))
= max(2, 7) = 7 //max 函数也要定义了才能用。case Cons(hd, tl) ⇒ max(hd, maxList(tl))
max(头, 剩余的冠军)剩余的冠军从哪来 —— 信任契约又登场了。
maxList(tl): 假装 maxList 已是造好的成品, 把 tl 塞给它, 它保证还你 tl 里的最大值, 别问它是怎么做到的。本层任务只剩把这个答案和 hd 送进 max 决赛
假装的原因
①tl 严格短一截, 必然触底
②底层答案是写死的, 不靠假装。底层是 case Cons(hd, Nil) ⇒ hd
maxList([5,3,9]) // 5 vs 剩余冠军
= max(5, maxList([3,9]))
= max(5, max(3, maxList([9]))) // 3 vs 更小范围的冠军
= max(5, max(3, 9)) // [9] 只剩一人, 不战而王
= max(5, 9) // 3 输给 9
= 9 // 5 输给 9, 尘埃落定注意形状: 一层层展开时什么也没算。只是欠下一层层"再回来比"的账。触底后从最里面往外逐层结算。
为什么终点是 Cons(hd, Nil) 而不是 Nil? 因为空列表没有最大值, 函数头上挂了 requires length(l) > 0。把空列表拒之门外。但这份合同每层递归都要守。如果只写 case Cons(hd, tl) ⇒ max(hd, maxList(tl)), 当列表只剩一个元素时, tl 是空的, 递归调用 maxList(Nil) 就违约了。所以必须加"只剩一人, 直接称王"这条, 让递归在触碰空列表之前刹车。合同不只管入口, 还管到每一次自我调用。
function maxListA(l: list<int>, maxSoFar: int): int
↑ ↑
要检查的剩余列表 目前为止见过的最大值。同一条 [5,3,9]
入口: maxListWithA([5,3,9]) → 拆出头5当初始擂主 → 转交 maxListA([3,9], 5)
账本版(边走边算): 朴素版(回程算账):
maxListA([3,9], 5) maxList([5,3,9])
= maxListA([9], max(3,5)) = max(5, maxList([3,9]))
= maxListA([9], 5) ← 3挑战失败 = max(5, max(3, maxList([9])))
= maxListA(Nil, max(9,5)) = max(5, max(3,9))
= maxListA(Nil, 9) ← 9上位 = max(5, 9)
= 9 ← 列表空, 交便签 = 9两边的形状差:
- 左边永远只有一层, 没有嵌套。每一行都是干干净净的 maxListA(短了的列表, 一个已经算好的数), 比较当场做完, 结果立刻写进第二个参数, 不欠账。所以走到 Nil 时, 答案已经躺在便签上。case Nil ⇒ maxSoFar 直接交货, 没有回程。
朴素版 maxList 只带一个包袱上路(列表), 账本版带两个, (列表 + 一个数), 这个数不是列表的一部分, 它是随身携带的便签, 上面永远写着"到目前为止的擂主是谁"。函数每走一步干两件事: 让新头挑战擂主, (max(hd, maxSoFar)), 把便签更新成胜者, 然后带着更短的列表和新便签继续走。
- 右边括号越叠越深, 每层只留下一句"回来再和5比""回来再和3比"的欠条。什么都不结算。直到触底才从最里往外还账。
①朴素版: 把所有人名单传到底, 再层层上报冠军
②账本版: 擂台赛, 擂主一路守擂, 打完即终。① 为什么账本版不需要 requires, 不需要单元素特判? 朴素版怕空列表, 是因为 Nil 时它两手空空, 交不出任何数; 账本版走到 Nil 时手里永远有便签, 交便签就行。空列表的难题被那个多出来的参数吸收了。
② 擂主哪来的第一任? 这就是 maxListWithA 那个入口包装的存在意义: 从列表里掏第一个元素当初始擂主。掏这一下要求列表非空, 所以 requires 挂在入口, 不挂在干活的函数上。
两函数分工: 一个体面(对外签名干净但要合同), 一个能干(对内多带个参数但百无禁忌)。
var newMaxSoFar := max(hd, maxSoFar); 比出胜者, 起个名, 传下去
maxListA(tl, newMaxSoFar)
和 maxListA(tl, max(hd, maxSoFar)) 等价。var 纯粹为了看着清楚。我写的:
datatype list<T> = Nil | Cons(hd: T, tl: list<T>)
function max(i: int, j: int): int{
if i < j then j
else if i > j then i
else i
}
function maxList(l: list<int>): int{
match l
case Nil => Nil //✗ 类型纪律: maxList 的签名承诺返回的是 int, 而 Nil 是列表 ⇒ 右边核对返回类型
case Cons(hd, tl) => max(hd, maxList(tl))
}空列表没有最大值可交的解法: 用 requires 把空列表拒之门外, 然后 Nil 的 case 整个不写
应该是:
function maxList(l: list<int>): int
requires l != Nil // 合同: 不收空列表
{
match l
case Cons(hd, Nil) => hd // 只剩一人, 直接称王(刹车)
case Cons(hd, tl) => max(hd, maxList(tl))
}requires 写在函数体花括号之前, 上面, 不是函数体第一行。
一旦挂上 requires, maxList(tl) 就成了违约现场: 列表剩最后一人时 tl 为空, 递归调用违反合同。所以必须补单人称王的刹车
list-recursion.dfy
datatype list<T> = Nil | Cons(hd: T, tl: list<T>)
// write these
function length<T>(l: list<T>): nat
function append<T>(l1: list<T>, l2: list<T>): list<T>
// some lemma might connect these two notions
// lemma ...长度和拼接之间有条显而易见的性质:
拼起来的长度 = 两段长度之和
lemma LengthAppend<T>(l1: list<T>, l2: list<T>)
ensures length(append(l1, l2)) == length(l1) + length(l2)
{}lemma 是拿逻辑锁死"代码没写错"的合同。
写任何递归函数, 问三问:
- 类型有几种情况?
- 终点那种情况答案是什么?
- 递归那种情况, 怎么用"更小的问题的答案"拼出当前答案?
对 length:
- 两种情况
- Nil 是空列表, 长度是0
- Cons(hd, tl) 是"一个头 + 一条尾巴", 长度自然是 1+尾巴的长度。尾巴的长度谁来算? length 自己。
function length<T>(l: list<T>): nat
{
match l
case Nil => 0
case Cons(_, tl) => 1 + length(tl)
}头是什么值不影响长度, 所以 hd 的位置放 _
length(Cons(1, Cons(2, Nil))): 1 + length(Cons(2, Nil)) →
1 + 1 + length(Nil) = 1 + 1 + 0 = 2套娃逐层剥开, 结果逐层往回加。
append函数
append: 拼接两条列表
append(l1, l2) 要把 l2 接到 l1 屁股后面。比如 [1,2] + [3] 得 [1,2,3]。
三问前有个先手判断: 对谁做 match? 拆 l1。理由: l2 整条会被原封不动接在后面, 不需要动它, 需要逐个搬运的是 l1 的元素。
- l1 分两种情况
- l1 是 Nil: 空列表接上 l2, 结果就是 l2 本身
- l1 是 Cons(hd, tl): 结果应该是"hd 打头, 后面跟着(把 tl 和 l2 拼好的东西)"
"tl 和 l2 拼好的东西"谁来做? append 自己。
function append<T>(l1: list<T>, l2: list<T>): list<T>
{
match l1
case Nil => l2 tl 是 l1 l1 为 Nil 时 ⇒ append(Nil, l2) 为 l2
case Cons(hd, tl) => Cons(hd, append(tl, l2))
} ↑ ↑ ↑
粘合剂 头 剩余的答案Cons(hd, append(tl, l2)) 在这里不是"拆", 是"装", 把 hd 重新包到递归结果的前面。
同一个构造子, 出现在 case 后面是拆, 出现在 ⇒ 右边是装。把 l1 一层层剥空, 剥到 Nil 时手里正好摊着 l2, 然后回程路上把剥下来的元素按原顺序一个个装回去。
append([1,2], [8,9])
= Cons(1, append([2], [8,9])) ← 剥下1, 留欠条: "回来给我套上 Cons(1, _)"
= Cons(1, Cons(2, append(Nil, [8,9]))) ← 剥下2, 又一张欠条
= Cons(1, Cons(2, [8,9])) ← 触底。l1 空了, 交出 l2, 这就是手里摊着 l2
= Cons(1, [2,8,9]) ← 还内层欠条, 2 套上去
= [1,2,8,9] ← 还外层欠条, 1 套上去。"装回去"完毕
append([5,3], [7])
= Cons(5, append([3], [7]))
= Cons(5, Cons(3, append(Nil, [7])))
= Cons(5, Cons(3, [7]))
= Cons(5, [3,7])
= [5,3,7]自己写 append 又写成
case Cons(hd, tl) ⇒ Cons(Cons(hd, append(tl)), l2)
✗一. append 少喂一个参数。append 的签名收两条列表, 每次调用都得两条齐上 append(tl, l2)
二. 外层 append(某坨东西, l2) 犯了坑位类型错误。Cons 的两个坑是死规矩, 第一个坑只吃单个元素, 第二个坑才吃列表。
三. 我想在这一行里把整个拼接画出来, 我的代码意图是左边组装好 l1 的前部分, 右边挂上 l2, 一步到位。它违反了递归分工的规律: 本层只干一层的活。只能撬一个头, 套一个头。整个剩下的难题快递给下一层。l2 不在这层里露面, 在 case Nil ⇒ l2 才端出来垫底。
Sum函数
function Sum(l: list<int>): int
{
match l
case Nil => 0
case Cons(hd, tl) => hd + Sum(tl) - l 分2种情况
- Nil 为空, 长度为0
- 当前的头, 加剩下的头之和。 加完就是整个列表里的 int 之和。