6260 notes: 枚举, 判别器, lemma, match

rainbow.dfy

datatype colour = Red | Orange | Yellow | Green | Blue | Indigo | Violet

function isRedWithEquality(c: colour): bool {
  c == Red
}

// write is-yellow with built-in discriminator(内建判别器)

date、point 都是一个构造器带字段。rainbow 这个是多个构造器,全都不带字段。竖线读作"或"。

这种全员无字段的 datatype 就是别的语言里的枚举(enum),比如 Rust:

enum Colour { Red, Orange, … }

两种罗列:

• 积类型管"并且"(字段罗列)
• 竖线管"或者"(选项罗列)

行话叫 sum type —— 积与和。

判别器

datatype 的每个构造器,Dafny 自动免费附赠一个判别属性:构造器名后加问号。

c.Red?、c.Yellow? 念作"c 是不是 Yellow 造的?",值是 bool。

function isYellow(c: colour): bool { c.Yellow? }

和 c == Yellow 零区别 —— 在这个文件里,无字段构造器上两者等价。

区别在带字段的 datatype:date 的世界没法问 d == Date。Date 是工厂不是值,拿盒子和工厂比是类型错误。只能问 d.Date? —— "是不是 Date 这条线出的"。

== 比的是两个值,? 问的是出身。

值相等要求字段全同,出身判别只看构造器。

(预告:到 Some(x) | None 时天天要用。)

fact-lemma.dfy

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

lemma fact6()                  // 引理,无参 lemma
  ensures fact(6) == 720       // unfolding:按定义展开
{}                             // 空函数体:无需人工证明

// a "universal property"(全称性质) about fact and <
forall n :: n < fact(n + 1)    // 需写归纳证明

证明全体才是 lemma 的本职 —— 从验证一个点,到证一条线。

lemma factPositive(n: nat)     // fact 和 < 之间恒真的关系
  ensures 0 < fact(n)
{}

dates.dfy

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

function centuryNumber(d: date): nat
{
  d.year / 100 + 1
}

// new syntax

:= 的两个现场:

① var:活在一个函数体内

② const:活在整个文件

const jan1_1900: date := Date(1, 1, 1900)

method Main()
{
  print "1900 is the in the ", centuryNumber(jan1_1900), "th century\n";
}

// some people dispute this; they *are* pedants, but…

整百年是关键条件:注意 off-by-one,差一引起 bug,边界上的归属要想清楚。

为什么要定义常量再传参?

一、名字即文档

二、一处定义,多处引用 —— 同一事实只写一遍

① const 把"这个值是什么"收拢到一行

② type vector3D 收拢的是类型

③ 函数收拢的是逻辑

三、常量能进规约

一个有名字的 const 在 lemma、assert、函数体之间通用。

重复是 bug 的温床。

centuryNumber 修正版

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

function centuryNumber(d: date): nat
  requires d.year >= 1
{
  (d.year - 1) / 100 + 1
}

// new syntax —— 为什么要用 :=?

const jan1_1900: date := Date(1, 1, 1900)
const jan1_1985: date := Date(1, 1, 1985)
const jan1_2000: date := Date(1, 1, 2000)

method Main() {
  print "1900 is in the ", centuryNumber(jan1_1900), "th century\n";
  print "1985 is in the ", centuryNumber(jan1_1985), "th century\n";
  print "2000 is in the ", centuryNumber(jan1_2000), "th century\n";
}

:= 的本职比赋值宽。它是"把右边的值,绑到左边的名字上" —— 绑定号。凡是"名字 ← 值"这个动作就用它。

四个现场

① var y := x * 10 + 5; —— var 绑定(function 体内,起名)

② d.(day := 1) —— 字段更新(新盒子的格子 ← 值)

③ i := i + 1; —— method 里赋值(旧名字 ← 新值)

④ const jan1_1900: date := Date(1, 1, 1900) —— 常量绑定(全局名字 ← 值)

= 和 := 用法对比

dates-with-month.dfy

datatype month =
  Jan | Feb | Mar | Apr | May | Jun |     // 十二个无字段构造器
  Jul | Aug | Sep | Oct | Nov | Dec

/* 30 days hath April, June, September and November,
   All the rest have 31, save February alone… */

function monthLen(m: month): nat
{
  match m {
  case Jan | Mar | May | Jul | Aug | Oct | Dec => 31   // | 读作"或",和 if 功能等价
  case Apr | Jun | Sep | Nov => 30
  case Feb => 28
  }
}

念法:"看 m 是哪个构造器造的,走对应的 case,箭头右边就是整个 match 表达式的值"。

// let's get this right for leap-years

match 的优越性:穷尽性检查

exhaustiveness —— 删掉一行就报错 "missing case"。

if 里漏写一个分支,else 默默兜底,没人发现,bug 上线。

match 把"考虑所有情况"变成强制要求。

加上闰年

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

predicate isLeap(y: nat) { y % 400 == 0 || (y % 4 == 0 && y % 100 != 0) }

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

method Main() {
  print "February of 2000 has ", monthLen(Feb, 2000), " days\n";
}

输出:

February of 2000 has 29 days.

两条收尾

function 的花括号里只能住表达式。

predicate / function / lemma 是声明,只能住顶层(文件一级,和 datatype、method 平起平坐)。