6260 notes: nominal typing, field update, requires, ensures

print is a universal tool

最原始的调试手段:程序行为不对,就在各处插 print,把中间值打出来看。

但这门课不行。print 是运行时看值,assert 是编译期间看真假。

蕴含消去:

a ==> b  ≡  !a || b
a ==> x  ≡  !a || x     在整个定义域上成立

lecture03

datatype date = Date(day: nat, month: nat, year: nat)

type vector3D 和 type date 都是 (int, int, int) 的透明绰号。而 datatype 造的是真正的新类型,不是绰号。

这个 date 和 (nat, nat, nat) 元组互不相认,和另一个结构相同的 datatype 也互不相认 —— 按名字区分,不按结构区分,即 nominal typing。

等号右边 Date(day: nat, month: nat, year: nat) 里,Date 叫构造器(constructor),是造这个类型的值的唯一工厂。三个字段有名字了,名字即文档。取值写 d.day,不是元组的 .0、.1、.2。

注意:小写 date 是类型名,大写 Date 是构造器名。

函数式更新

这个文件真正的新语法:

d.(day := 1, month := 1)

念作:"给我一个新日期,它和 d 一样,除了 day 换成 1、month 换成 1。"

year 没提,原样带过来。

关键在"新"字。回想 function 的铁律:没有可变状态,任何东西都不能被修改。

那想"改"一个字段怎么办?不改,造一个改好了的副本。 d 本身毫发无损,拿到的是另一个值。

这跟 nat 世界"不让负数出现"是同一个哲学:让违规无从发生。行话叫 functional update。

function makeFirstOfJan(d: date): date
{
  d.(day := 1, month := 1)
}

整个函数读作:收一个日期,返回"同年一月一日",没有一处赋值、修改。

day-after

// What about a day-after function?

进位的麻烦在于:同一个"加一",在不同输入上要动的字段数不同,所以函数体必然是 if 的级联。

Ver 1.0 —— 我最初的伪代码

if 日 = 30              // 先加还是先判?先判
    day + 1
    日 = 1
if 月 = 12
    月 = 1    年 = 年+1
else
    月 = 月 + 1

最特殊的情况放最前面,最普遍的情况放最后面兜底:

① 如果今天是年末,则:day 归 1,month 归 1,year 加 1

② 否则,如果今天是月末,则:day 归 1,month 加 1

③ 否则,月中绝大多数日子,则:day 加 1,其余不动

分支的排列规矩:特殊压倒一般,越苛刻的条件越先查。这是 if 级联的第一定律。

Ver 1.1 —— 然后我写的代码

function dayAfter(d: date): date {
  if d.day == 30 && d.month == 12 then      // 条件里是 == 不是 =
    Date(1, 1, d.year + 1)                  // 用构造器 Date 整个重造
  else if d.day == 30 then                  // 不必写 month != 12,else 本身就是信息
    d.(day := 1, month := d.month + 1)
  else
    d.(day := d.day + 1)
}

为什么要用 d.day, d.month, d.year?

d 是一整个盒子,不是三个散落的数。签名 dayAfter(d: date) 里,进来的参数只有一个,名字叫 d,类型是 date。

datatype date = Date(day: nat, month: nat, year: nat)

这行定义说了,date 是一个装着 day、month、year 三个格子的盒子。所以函数收到的是一个完整的盒子。

在函数体里,day 这个名字不存在。 作用域里只有一个名字 d。day 不是变量,是盒子上某个格子的标签,必须先指着盒子再指格子。

d.day = "d 这只盒子的 day 格"。那个点就是"的"。

① 元组:xy.0、xy.1 ← 格子按位置叫:0 号、1 号

② datatype:d.day、d.month ← 格子按名字叫:month、day

再看两种操作:

① d.(day := 1) —— 造:造一只新盒子,day 格换成 1,其余格子照抄 d

② d.day —— 读:取出 d 的 day 格的值

只有读与造,没有改。

Date(1, 1, d.year + 1)

为什么前两个位置是裸的 1,第三个位置必须是 d.year 不是 year?

因为填进去的 1 不来自任何盒子,而第三格的值要从旧盒子 d 里读出来再加。

凡是从已有盒子里取,就必须"点谁,取谁"。

一、d.() 和 Date() 等价吗?

功能殊途同归,都产出一个新 date,出发点相反。

① Date(1, 1, d.year+1) 是从零起盖,三个格子必须亲手填满,少一个不给过

② d.(day := 1, month := 1) 是照着旧的翻新 —— 以 d 为底本,点名要换的格子,没点名的自动照抄

所以用哪个取决于要换几格。三格全换,盖新的省事;否则只点一两格的名。

二、为什么翻新要写 := 1,盖新的直接写 1?

因为两者需要的信息量不同。

Date(1, 1, x) 靠位置认格子,定义里 day 排第一、month 排第二 —— 位置即身份,不用报名字。

而 d.() 只动一部分格子,不报名怎么知道这个 1 给 day 还是 month?

位置定位 vs 点名定位。

三、:= 是什么,为什么不用 =?

Dafny 里:

① == —— 问:两边相等吗?产出 true/false。比如 d.month == 12

② := —— 给:把右边的值放进左边的格子/名字。比如赋值、var、绑定、字段更新

③ = —— 定义:几乎只在声明里出现。意为:从此这个名字的意思是…

四、month := d.month + 1 里两者是什么关系?

• month:收货地址
• d.month:取货来源

① d.month —— 去旧盒子 d 里读 month 格,取出 8(读旧盒子,必须点谁取谁)

② 加 1 得 9

③ month := —— 把 9 放进新盒子的 month 格(新盒子此刻正在建造中,还没有名字可点)

dayAfter(Date(15, 8, 2026))

五、为什么传参要写 Date(15, 8, 2026) 不能写 (15, 8, 2026)?

签名里 d: date 和 Date() 是什么关系?

datatype date = Date(day: nat, month: nat, year: nat)

date 是真类型,不是元组绰号。而 (15, 8, 2026) 造出来是元组,类型 (int, int, int)。

dayAfter 签名写 d: date —— 合同规定只收 date。nominal typing,元组和 date 结构再像也不认。这正是从 type 升级到 datatype 的目的:不让元组随便冒充。

要造 date,只有一扇门:构造器 Date。签名 d: date 说"此处收这一类的值",Date() 造"这一类的一个具体值"。

类型属于类,值是成员。

新文件没有新世界,只是旧零件的新排列。

组合性

函数调用表达式的类型 = 该函数签名的返回类型。

但大图景是:每一个表达式都有类型,而且复合表达式的类型由零件的类型逐层算出来。函数调用只是其中一条规则。

任何一个大表达式,类型检查器都是从叶子往根一层层算上来的。

零件类型决定整体类型的这条原则叫组合性(compositionality),它是静态类型语言的地基。

simple-requires.dfy

datatype point = Point(x: int, y: int)

function gradient(p1: point, p2: point): int
{
  // "rise over run"
  (p2.y - p1.y) / (p2.x - p1.x)
}

问题:p1 和 p2 的 x 坐标相同时,分母是 0。两点竖直排列,斜率无定义 —— 数学里这条线是"斜率不存在",代码里这是除以 0。

nat 减法要证结果非负,返回 nat 要证承诺兑现,而除法要证分母非零。这行代码里没有任何东西挡住 p1.x == p2.x 的输入,所以证不出来。

回想 absDiff 的思路,有个土办法:

if p1.x == p2.x then 0 else (p2.y - p1.y) / (p2.x - p1.x)

但竖直线的斜率不是 0,却返回 0,和事实不符。

Dafny 的打法:不处理非法输入,直接在合同里拒收。

function gradient(p1: point, p2: point): int
  requires p1.x != p2.x
{
  (p2.y - p1.y) / (p2.x - p1.x)
}

requires 念作"调用前提"。每个调用点,验证器反过来核查调用者能不能证明这个前提。

语言内建的前提有:nat 减法、返回类型、终止性、除零。

requires 把写前提的笔交到 programmer 手中,和语言立的规矩待遇相同 —— 编译期强制要求,违者不过。

规约与实现分离是整门课的骨架。

三种 error

① parse error —— 话没说囫囵

② type / resolution error —— 话说对了,但零件对不上

③ verification error —— 语法类型全对,但证明不过

simple-lemma.dfy

lemma simple(x: int, y: int)
  ensures x < 10 + y ==> 2 * x - 2 * y < 20
{}

lemma 没有函数体,不调用它,不产出值。全部使命在 ensures 那一行:向验证器宣布一条数学命题,并要求验证器证明它。

参数 (x: int, y: int) 在 lemma 里不是"待传入的输入",而是全称量词 ∀x∀y。

print 有限,lemma 证无穷。

requires 拒收界外输入,蕴含对界外输入自动放行。

关于花括号:

• 空花括号 {} = 体在此,内容为空,请去证明
• 无花括号 = 体缺席,当公理,跳过证明

两条报错的读法:

• precondition could not be proved —— 调用方违约
• postcondition could not be proved —— 声明者吹牛

simple-ensures.dfy

function makeItBigger(i: int): int
  ensures makeItBigger(i) > i

ensures 挂在 function 上,承诺的主角是返回值。

说的是:"我吐出的那个值,保证满足这条性质" —— makeItBigger(i) > i,返回值严格大于输入。

makeItBigger(i) 指的是"本函数的返回值"。这是 function 世界特有的写法:函数名即结果名。

function makeItBigger(i: int): int
  ensures makeItBigger(i) > i    // 注意:ensures 写在函数体前面

{ i + 1 }                        // 为什么不写成 { i = i + 1 }?

单行才需要离花括号一格。函数体一旦换行,花括号各占一行或挂在行尾。

i + 1 > i 对任意 int 恒真(int 无上界,不怕溢出)。这是 Dafny 任意精度整数又一次悄悄兜了底 —— 64 位语言这条在 MAX_INT 处会溢出。

两种"给定一半问另一半":

① lemma:命题在此,请证明。给定式子问真假

② 带 ensures 的空 function:性质在此,请实现。给定规格问哪个函数满足它

"规约与实现分离" —— 这是规约先行(spec-first)的最小标本:先写"什么算对",再补"怎么做到"。

规格划定的是合法解的集合,实现只需是其中一员。

为什么 { i + 1 } ✓ 而 { i = i + 1 } ✗

一、语法层:花括号里要的是表达式

function 的函数体规则:体就是一个表达式,表达式的值即返回值,没有 return。i + 1 是表达式,值是 i + 1。

i = i + 1,按 Dafny 符号表,单 = 只在声明里合法。这里直接 parse error(话没说囫囵)。

就算写成 i == i + 1,合法表达了问句"i 等于 i 加 1 吗?",值永远是 false。

二、我想写的其实是赋值

"把 i 更新成 i+1,然后函数把 i 交出去" —— 这个模型在 function 世界整体非法。

这是世界观问题。

function 活在数学世界,数学里没有"变"。

比如 f(x) = x + 1,x 在等号右边没有被"改"过,x 是个名字,指着一个值。

f(3) = 4 不是 3 变成了 4,而是照着 3 算出了 4。

function 的花括号等于等号右边:

在描述"输出是输入的什么函数",不是在指挥"输入该怎么变"。

所以在这里根本没有赋值这个动作可用。所有的更新其实全是造新的,用的是 := 绑定,而非修改。

那"真赋值"在 method 里 —— method 世界有可变变量,i := i + 1; 是合法语句,分号结尾,i 的值真的被覆盖。

① function 描述 what(是什么),只能算,不能令

② method 指挥 how(怎么变)

requires-ensures.dfy

function makeItSmaller(i: int): int
  ensures makeItSmaller(i) < i

// think about other types

(i: int) 是参数表,后面跟的 : int 是返回类型。

递减 ≠ 压在对角线下

严格递减函数 f 保证 f(a) < f(b) 当 a > b —— 它比较的是两个输出之间的关系。

但这条 ensures 要的不是这个,它要 f(i) < i:输出和自己的输入比。

这是两个不同的性质,谁也不蕴含谁。

反例:f(i) = i - 1 满足输出恒小于输入,但它严格递增。

后者这类"输出被输入压住"的性质,数学叫 deflationary(压缩性),和 monotone(单调性)正交。

合同只要求压在对角线下,最便宜的兑现是平移 i - 100。

规格划合集,实现挑一员。

换成 (i: nat): nat 写得出来吗?

i = 0 时,需要一个比 0 还小的数 —— 写不出来。两个方向:

① 改 requires:剃掉 0

② 改返回类型为 int

个人迷思: 我原本写的是"改 ensures:改为 int 返回类型"。它俩不是一层 —— ensures 是性质,int 返回类型是国籍。

类型不是 require 出来的

不能写成 requires i: int。

因为 requires 后面要 bool 表达式(比如 requires p1.x != p2.x,一个问句),而 i: int 不是问句,是声明 —— 它是签名里的话,不是条件。

类型是在参数表(签名里圆括号以及里面的东西)里用冒号钉死的。圆括号结束、直到花括号之前的就是返回类型。

三层各管各的

① 类型:身份,全程有效,写在参数表和返回位

② requires:入场条件,bool 表达式,管调用者

③ ensures:出场承诺,bool 表达式,管实现者

nat = x: int | x >= 0

两种改法

① 加 requires i > 0

function makeItSmaller2(i: nat): nat
  requires i > 0
  ensures makeItSmaller2(i) < i
{ i - 1 }

requires 和 ensures 各管各的,加了前者不能免掉后者。不写 ensures,验证器就不承诺 —— 调用后拿到的值什么性质都不带。

② 改返回类型为 int

function makeItSmaller3(i: nat): int
  ensures makeItSmaller3(i) < i
{ i - 1 }

同一文件里函数名必须唯一,所以写成 makeItSmaller2 和 makeItSmaller3。

减法本身要过"结果是 nat(≥0)"的审。