Lab01,三大位置规则,datatype,match,requires/ensures

hello.dfy：总览

读这个文件之前需要知道的全部背景:

Dafny 是一门"带验证器的编程语言"。写代码,同时写下对代码的断言(它应该满足什么性质),然后运行 dafny verify 文件名.dfy——验证器会用数学方法检查:断言是否对所有可能的输入都成立。不是跑几个测试用例——是全部输入,一个不漏。这就是它和普通语言的根本区别。

注释语法:// 到行尾;/* ... */ 块注释。注释不参与验证。

本文件相对原件改了两处,否则无法通过解析:原文件第 175 行末尾有一个孤立的 "|" 字符(粘贴事故),已删除;isLeapYear 里 "0then" 缺空格,已补。其余代码与原件逐字相同。全文在 Dafny 4.11.0 下验证通过:18 verified, 0 errors。

method：语句的世界

method 是"过程式"的代码块:一串按顺序执行的语句,可以打印、可以修改变量。Main 是特殊名字:程序的入口,dafny run 时从这里开始执行。本课程里 method 只是配角(用来跑 print 看结果);主角是 function 和 lemma。三样基础语法:var d := 表达式; 声明并赋值,:= 是赋值符号,每条语句以分号结尾;print d, "\n"; 打印;变量不写类型时 Dafny 自己推断。

method Main(){
    var d := distSquared((3, 2));           // (3, 2) 是一个二元组
    print d , "\n";
    var dotp := dotProduct((2,3), (4, 5));
    print dotp , "\n";
    var perpend := perpendicular((1,0), (0,5));
    print perpend, "\n";
    var div := divides(6, 2);
    print div, "\n";
    var inrange := inRange(2, 3, 4);
    print inrange, "\n";
    var cen := withTax(100);
    print cen, "\n";
    var s := area(shape.Rectangle(2, 3));   // 构造一个"形状"值
    print s, "\n";
    var m := monthLen(month.Jun, true);
    print m, "\n";
    var expx := exp(2, 3);
    print expx, "\n";
}

function：表达式的世界

function 是数学意义上的函数:给输入,算输出,别的什么都不做。剖析定义的每一块:v : (int,int) 参数 v,类型是一个由两个整数组成的元组 tuple,类型标注永远是 名字 : 类型;最后的 : int 是返回类型;花括号里只放一个表达式,它就是返回值——没有 return,没有分号,不能写语句。这是 Dafny 三大位置规则的第一条:

◆ function 体 = 表达式的位置。

取元组的分量用 .0 和 .1(从 0 数起)。

function distSquared(v : (int,int)) : int
{
    v.0 * v.0 + v.1 * v.1   // 向量 v 的长度平方 = x² + y²
}

function dotProduct(u : (int,int), v : (int,int)) : int
{
    u.0 * v.0 + u.1 * v.1   // 点积：对应分量相乘再相加
}

predicate：返回 bool 的缩写

predicate(谓词)就是返回类型为 bool 的 function,只是省去 : bool 的一种缩写。数学上,谓词 = 一个关于输入的判断。

◆ 表达式版的 if:if 条件 then A else B 整体是一个表达式,值为 A 或 B。else 不能省——表达式必须有值。(对比语句版的 if:出现在 method / lemma 体内,带花括号,可以没有 else。同一个词,两种身份,位置决定身份。)

◆ 风格备注:if c then true else false 与直接写 c 完全等价。官方这里写了展开版;考试里两种都对,但直接写 c 更体面。两向量垂直 ⟺ 点积为零,本可一行:dotProduct(u, v) == 0。

predicate perpendicular(u : (int,int), v : (int,int))
{
    if dotProduct(u, v) == 0 then true else false
}

nat 与 % 的定义域

nat 是"自然数"类型:≥ 0 的整数,是 int 的子集类型;用 nat 做参数,等于免费获得一条前置条件"参数 ≥ 0"。

divides(m, n) 判断 n 能否整除 m(注意参数顺序:m 是被除数)。关键点:

◆ m % n 只有在 n != 0 时才有定义。Dafny 会拒绝任何可能"除以零"的表达式——不是运行时报错,是验证阶段直接不通过。

◆ 那第二个分支为什么合法?因为 && 是短路的:在 n != 0 && m % n == 0 里,只有左边为真时才需要看右边,所以 Dafny 只要求 m % n 在"n != 0 成立"的前提下有定义。用条件的顺序保护危险表达式——这个手法贯穿全课程,lab04 的 div12 会再见到它(换成 requires 的顺序)。

◆ 链式比较:lo <= x <= hi 是合法 Dafny,等价于 lo <= x && x <= hi,同方向的比较可以连着写。

function divides(m : nat, n : nat) : bool
{
    if (m == 0 && n == 0) then true
    else if (n != 0 && m % n == 0) then true
    else false
}

predicate inRange(lo : int, x : int, hi : int)
{
    if lo <= x <= hi then true else false
}

requires：前置条件

requires 写在签名和函数体之间,是对调用者的要求:"想用我,先保证这个条件"。验证器会在每个调用点检查它。

◆ 三大位置规则第二条:requires / ensures 里放的是命题(可判真假的断言),不是语句。

requires 有两种动机:(a) 保证函数体里的表达式有定义(除零、取空列表的头……);(b) 排除"数学上能算、语义上荒谬"的输入——本例属于这种:负的金额算税没有意义,尽管 cents / 10 对负数也能算。

◆ 函数体内的 var:var tax := ...; 表达式 是表达式的一部分(数学里的 let),给中间值起名字,分号后面跟着最终表达式。别和 method 里的赋值语句混淆——形似,位置和本质不同。

◆ 整数除法向下取整:105 / 10 == 10,不是 10.5。

function withTax(cents : int) : int
  requires cents >= 0
{
    var tax := cents / 10;
    cents + tax
}

datatype：代数数据类型

datatype 定义一种新类型,穷举它的所有构造方式。最简单的形态是枚举;构造子也可以带字段——竖线 | 读作"或者",构造值时写 shape.Rectangle(2, 3),类型名前缀在无歧义时可省略。

datatype light = Red | Orange | Green

datatype shape =
    Rectangle(height : nat, width : nat)
  | Square(side : nat)
  | Triangle(base : nat, height : nat)

match：模式匹配

match 按构造子拆开一个 datatype 值。读作:如果 s 是用 Rectangle 造出来的,就把它的两个字段取名为 h、w,然后算右边的表达式。case 必须穷尽所有构造子——漏一个,验证器报错。这保证你永远不会忘记处理某种情况。

◆ match 出现在 function 体里时,整体是一个表达式(每个 case 的右边也是表达式)。它还有语句形态,lemma 里见。

◆ 多模式合并:case Apr | Jun | Sep | Nov => 30,几个构造子共享同一个结果,写一次即可。注意这里"月份"被建模成 datatype——lab04 会给出另一种建模(nat 0..11 加 requires),两种方案的代价对比到时讲。

function area(s : shape) : nat
{
    match s
    case Rectangle(h, w) => h * w
    case Square(s) => s * s        // 这个 s 是新名字，遮住了参数 s
    case Triangle(b, h) => (b * h)/2
}

datatype month =
    Jan | Feb | Mar | Apr | May | Jun |
    Jul | Aug | Sep | Oct | Nov | Dec

function monthLen(m : month, isLeap : bool) : nat
{
    match m
    case Feb => if isLeap then 29 else 28
    case Apr | Jun | Sep | Nov => 30
    case Jan | Mar | May | Jul | Aug | Oct | Dec => 31
}

闰年规则的 if 链版本:400 整除 → 闰;否则 100 整除 → 平;否则 4 整除 → 闰;否则平。判断顺序承载了规则的优先级。 lab04 有一个一行的"纯逻辑"版本,两者等价,届时对照。

predicate isLeapYear(year : nat)
{
    if year % 400 == 0 then true
    else if year % 100 == 0 then false
    else if year % 4 == 0 then true
    else false
}

lemma 与 assert

lemma(引理)是一段"证明":不产生值,只让验证器确认一个事实。

◆ 三大位置规则第三条:lemma 体 = 语句的位置。 assert 命题; 就是一条语句,意思是"验证器,请在此处证明这个命题"。证不出来 → 报错。

下面三条是测试引理:拿具体数字喂给函数,让验证器算一遍确认结果。注意,验证器是真的把函数按定义展开算出来的,不是跑程序。

一个值得较真的细节:这里的写法是 assert 放体内、ensures 空缺。这样验证时确实检查了事实,但引理对外什么都没承诺(ensures 为空 = 调用它得不到任何信息)。惯用的测试引理写法是反过来:lemma isLY2024() ensures isLeapYear(2024) {}——把命题放进 ensures,体留空。两种都能过验证;后者才是可被别的证明引用的形态。体会一下:同一个命题,放 assert(体内语句)和放 ensures(对外契约),角色完全不同。

lemma isLY2024()
{
    assert isLeapYear(2024) == true;    // == true 可省：assert P; 即可
}
lemma isLY1900()
{
    assert isLeapYear(1900) == false;   // 可写 assert !isLeapYear(1900);
}
lemma isLY2000()
{
    assert isLeapYear(2000) == true;
}

递归与停机

函数调用自己。递归必须停机,Dafny 要检查这一点。规则:每次递归调用,某个度量必须严格变小、且有下界。没写 decreases 时,Dafny 默认拿参数本身当度量:这里 p : nat 每次减一、又不会低于 0,自动通过。往后遇到 Dafny 看不出来的递归,才需要手写 decreases(lab03 的 Part C)。

function exp(m : nat, p : nat) : nat
{
    if p == 0 then 1 else
    m * exp(m, p-1)
}

斜率 = Δy / Δx,requires 保证分母不为零(这里更强:> 0)。◆ 但类型是 int:整数除法截断。gradient((0,0),(2,1)) == 0,真实斜率 0.5 被抹掉了。requires 能保证"有定义",救不了"类型选得不合适"。看见 int 除法就要想一下截断。

function gradient(p1 : (int,int), p2 : (int,int)) : int
  requires (p2.0 - p1.0) > 0
{
    (p2.1 - p1.1) / (p2.0 - p1.0)
}

ensures：后置条件

ensures 是函数对调用者的承诺:"我的返回值满足这个命题"。验证器负责检查函数体确实兑现承诺;此后所有调用点免费获得这条知识。在 ensures 里提到返回值的方式:直接写函数调用自身 makeItBigger(i)。(另一种写法是给返回值命名,课程后面见。)

function makeItBigger(i : int) : int
  ensures makeItBigger(i) > i
{
    i + 1
}

阶乘:if n < 2 合并了 0 和 1 两个基础情况(0! = 1! = 1)。原件把题目要求的 ensures 写成了体内 assert(TODO 注释还留着)。两种形态的差别上面 isLY2024 处已讲——验证都能过,但题目点名要 ensures,考试按题目来:lemma factTest1() ensures fact(4) == 24 {}。

function fact(n : nat) : nat
{
    if n < 2 then 1 else n * fact(n - 1)
}

// Claim: fact(4) equals 24.
lemma factTest1()
// TODO: write the ensures for "fact(4)"
{ assert fact(4) == 24; }

// Claim: fact(6) is greater than 100.
lemma factTest2()
// TODO: write the ensures that claims that 6! is strictly larger than 100
{ assert fact(6) > 100; }

预告：递归数据类型

datatype 的构造子字段可以是这个类型自己——于是有了链表:一个 list<T> 要么是空表 Nil,要么是 Cons(头元素, 剩余的表)。<T> 是类型参数(泛型):list<int>、list<bool> 共用一份定义。[1,2] 就是 Cons(1, Cons(2, Nil))。

这三个函数是整门课的主旋律,此处只需先看出它们的共同骨架:match 拆两种情况;Nil 直接给答案;Cons 处理头、递归尾。

datatype list<T> = Nil | Cons(hd : T, tl : list<T>)

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, A : list<int>) : bool
{
    match A
    case Nil => false
    case Cons(y, ys) => if y == x then true else member(x, ys)
    // 等价一行：y == x || member(x, ys) —— lab03 的官方版就这么写
}