Dafny
lijiahai
2022-03-25
目录

各种推导式

# 各种推导式

K. Rustan M. Leino Manuscript KRML 267, 27 May 2019

摘要 Dafny有许多类似推导式的结构。本文描述并比较了这些结构，展示了它们在语法和语义上的比较。

Dafny支持普遍量化和存在量化，以及用于“证明”普遍量化表达式或“利用”存在量化表达式的结构。[0]节(http://leino.science/papers/krml267.html#sec-quantifiers)描述了Dafny中的这些逻辑量词。第[1]节(http://leino.science/papers/krml267.html#sec-proof-features)显示了在推理量词时可以使用的程序语句，并指出了各种语法形式的差异。

集合推导式和映射推导式类似于量词，因为它们引入了范围超过特定值的绑定变量。[2]节(http://leino.science/papers/krml267.html#sec-sets-and-maps)展示了这些理解的一般和常见形式。

# 量词

# 基本的量词的语法

在数学教科书和论文中，我们熟悉的全称量词采用了类似的符号。它说谓词对所有的值都成立。在编程语言行话中，我们说它是一个绑定变量，其作用域是量词的主体。也就是说，任何自由出现的in都被绑定到量词所引入的。

在Dafny中，同一个全称量词被写成forall x:: P。从解析的角度来看，量词的主体“尽可能地”扩展。因此，程序片段

forall x :: R ==> Q
1

解析为

(forall x :: (R ==> Q))
1

而不是

(forall x :: R) ==> Q
1

请注意，“尽可能”不限于行尾。例如，一个常见的陷阱是编写(这里显示的是一个前置条件)

requires
  forall x :: R ==> Q &&
  S
1
2
3

意图是forall x:: R ==> Q和S是两个独立的前提条件。与此相反的是，这里所写的声明的意义是

requires (forall x :: (R ==> (Q && S)))
1

如果你打算写量词和S的连词，那么正确的语法是

requires
  (forall x :: R ==> Q) &&
  S
1
2
3

存在量词的一个熟悉的数学符号是。它说谓词对于某个值成立。在Dafny中，语法是exists x:: P .0 (opens new window)

# 绑定变量的类型

Dafny中的每个变量都有一个类型。通常，绑定变量的类型是推断的，但Dafny也允许显式声明该类型。例如,

forall x: X :: P
1

声明x的类型为x。为了简洁，并展示编写量词和推断的典型方法，我将在本文中省略类型，但请记住，如果愿意，您可以随时包含它们。

当约束变量从某个集合中提取时，量词的常用数学符号是。这个表达式的dafny式表示为

forall x in S :: P  // error: syntax error
1

然而，这是不正确的Dafny语法，因为它使用了一个集合成员谓词，其中只期望绑定变量(可选的，带有类型)。在Dafny中这样一个量词的正确写法是

forall x :: x in S ==> P
1

# 多个绑定变量

一个限定符可以有一个以上的绑定变量。例如,

forall x, y :: P
1

P对于所有的x和y都成立。它在逻辑上等同于嵌套的量词

forall x :: forall y :: P
1

就此而言，它在逻辑上也等价于

forall y :: forall x :: P
1

Dafny的常见做法是使用多个变量的量词，而不是嵌套的形式，如果没有其他原因，只是为了更简洁。1 (opens new window)

如果您编写了一个绑定变量列表并显式地给出了类型，请注意，每个给定的类型只适用于它之前的变量。例如,

forall x: X, y: Y :: P
1

x的类型是x, y的类型是y。如果只包含y类型，如

forall x, y: Y :: P
1

那么你说y的类型是y而x的类型是可以推断的。换句话说，你可以认为这个“:”比“，”具有更强的约束力。

# 量词主体的典型形式

全称量词的主体通常是一种含义，如in

forall x :: R ==> P
1

你可以从以下几个方面来解读:

"对于所有的x，意味着R ==> P成立"

"对于所有的x， R意味着P "

"对于所有的x，如果R成立，那么P也成立"

然而，这个含义的先行词(R)通常起到限制(不仅仅是x的类型)所考虑的x的值的作用。换句话说，“R”告诉你“x”的范围。在这种情况下，你可以从下面的一种方式来解读上面的量词:

"对于所有满足R的x， P成立

"对于所有的x，使R成立，P "

"对于所有的x(其中x满足R)， P保持"

“对于所有的x[为R插入你自己的描述性阶段]，P”

作为最后一个短语的具体实例，你可以读到forall x:: x in S ==> x % 2 == 0 As

"对于S中的所有x， x是偶数"

你可以读到forall i:: 0 <= i < a. length ==> a[i] == 5 as

"对于数组a的每个下标i， a -sub- i是5 "

和我刚才说的全称量词类似，存在量词的典型形式是连词，比如

exists x :: R && P
1

例如：

exists x :: x in S && x % 2 == 0

exists i :: 0 <= i < a.Length && a[i] == 5
1
2
3

再把R看成是告诉你x的范围，你可以把这些存在量词看成

"在S中有一个x，其中x % 2 == 0适用"

"在a中有一个索引i，使a -sub- i等于5 "

在Why3 [1 (opens new window)]之后，如果你将R ==> P作为存在量词的主体，Dafny会发出警告，因为这几乎总是一个用户错误(一个打字错误或一个思考-o)。如果这真的是你想要写的，你可以通过编写以下任何表达式来抑制警告:

exists x :: (R ==> P)
exists x :: !R || P
exists x :: P <== R
1
2
3

# 范围谓词

为什么我要花一页来告诉你量词的发音?因为这个讨论强调了一个事实，条件R，在任何一个

forall x :: R ==> P
exists x :: R && P
1
2

扮演着特殊的角色，尽管“R”实际上只是这些量词主体的一部分。事实上，其他人已经为量词采用了一种表示法，该表示法为这个范围谓词 R设置了一个特殊的位置。下面是一些例子:
Universal quantifier Existential quantifier Source
Dijkstra [3 (opens new window)]
Chandy and Misra [2 (opens new window)]
Gries and Schneider [4 (opens new window)]
\forall X x; R; P \exists X x; R; P JML [5 (opens new window)]

(在上面的JML中，X表示X的类型。)在使用这些符号的教科书中，经常有人说:“为了简洁，如果‘R’是‘正确’的，或者是根据上下文理解的，那么它(对于上面的一些作者来说，一些相邻的标点符号)就被省略了。”这些缩写形式是:
Range listed separately Range true or omitted Source
Dijkstra [3 (opens new window)]
Chandy and Misra [2 (opens new window)]
Gries and Schneider [4 (opens new window)]
\forall X x; R; P \forall X x;; P JML [5 (opens new window)]

还有更多的。通过使用一些区分“R”和“P”的符号，量词的德摩根定律看起来特别好:

回到Dafny。如果您喜欢将绑定变量的范围从量词主体的其余部分分隔开的符号，那么您将很高兴地了解到，您也可以在Dafny中这样做。语法是:

forall x | R :: P
exists x | R :: P
1
2

# 用于量词推理的程序语句

Dafny包含了一些在推理涉及量词的程序或定理时非常有用的证明特性。它们的语法与量词相似，但也有区别。

# 聚合语句

Dafny中的forall语句是一个聚合语句:它具有执行多个同时操作的效果。当这句话用于证明时，其形式如下:

forall x | R
  ensures P
{
  S;
}
1
2
3
4
5

它用于建立属性forall x | R:: P，即forall x:: R == >p。它是通过检验命题S为任何满足R的x建立P来实现的。在逻辑中，这个命题的结果被称为“普遍引入”。

举个简单的例子，假设你有一个引理可以证明n <= Fib(n)对于任何n至少是5，其中Fib是通常的Fibonacci函数:

function Fib(n: nat): nat {
  if n < 2 then n else Fib(n-2) + Fib(n-1)
}

lemma FibProperty(n: nat)
  requires 5 <= n
  ensures n <= Fib(n)
{
  // some proof goes here
}
1
2
3
4
5
6
7
8
9
10

这个引理给出了一个给定n的属性n <= Fib(n)。但假设你想让这个性质以普遍量子化的形式存在。也就是说，你要证明下面的引理:

lemma FibPropertyAll()
  ensures forall n :: 5 <= n ==> n <= Fib(n)
{
  // some proof to go here
}
1
2
3
4
5

我们怎么写这个证明呢?2 (opens new window)

答案是对每个n调用FibProperty一次。一次。对于“n”有无数个不同的值。这就是你对聚合语句forall所做的:

forall n | 5 <= n
  ensures n <= Fib(n)
{
  FibProperty(n);
}
1
2
3
4
5

一般来说，forall语句的主体要比单个引理调用复杂得多。但是当主体是只是一个引理调用或只是一个calc语句时，Dafny会自动推断ensure子句，所以你可以省略它:

forall n | 5 <= n {
  FibProperty(n);
}
1
2
3

# 存在引入与排除

使用存在量化还使用了一系列的证明特征。我将通过写一个证明来证明斐波那契数可以是任意大的:

lemma EverBigger(k: nat)
  ensures exists n :: k <= Fib(n)
{
  // proof to go here
}
1
2
3
4
5

让我们从一些简单的例子开始证明，比如当k很小的时候，比如0或1:

if k < 2 {
  // simple case: proof for k being 0 or 1 goes here
} else {
  // difficult case: proof for larger k goes here
}
1
2
3
4
5

Dafny不能自动证明这两种情况，所以我们需要自己给出更多的证明。

为了证明这个引理在简单的情况下，它足以向验证者证明存在量词持有的一个特定的n。也就是说，我们想给存在量词一个见证。一个这样的见证是1，因为k <= 1 == Fib(1)。另一个这样的见证是12，因为k <= 144 == Fib(12)。另一个这样的见证是k，因为在我们的简单例子中k <= k == Fib(k)。让我们继续这个，所以我们在引理主体的“if”语句的“then”分支中添加一个断言:

assert k <= Fib(k);
1

Dafny将证明这个断言3 (opens new window)，然后会注意到k是一个证明后置条件的存在见证。在逻辑中，这被称为“存在论导言”。这意味着，如果你有一个满足特定属性的值，那么这个值就存在。换句话说，如果你有一个“在你手中”的价值，那么这个价值就存在了——这似乎是如此明显，以至于我们谈起它时几乎会感到尴尬(你的邻居听到你以这个为生肯定会认为你疯了)。

那么这个棘手的案例呢?我们可以通过归纳法来证明，首先得到一个n，它的斐波那契值至少为k-1，然后再从中构建一个更大的斐波那契值。首先，我们在“k-1”上递归地调用引理:

EverBigger(k-1);
1

这让我们获得了EverBigger(k-1)的后置条件。为了在我们的证明中明确地写下这一点——为了检查验证者是否得出了我们期望从引理调用中得到的结论，并提醒我们自己什么属性——我们可以写一个断言:

assert exists n` :: k-1 <= Fib(n`);
1

好到目前为止。接下来，我们想构造一个至少比Fib(n)大1的斐波那契数，因为这样可以完成证明。但是我刚才提到的n是什么?上面的所有断言都告诉我们存在这样的“n”。我们希望有这样一个“n”在我们手中，这样我们就可以使用它。

从我们知道存在的东西到“在我们手中”的东西被称为“Skolemization”或“existenelimination”。你在Dafny中通过assign-such-that语句实现:

var m: nat :| k-1 <= Fib(m);
1

这个语句引入了一个局部变量m，并给它一个任意值，满足k-1 <= Fib(m)。当然，如果不存在这样的值，这是不可能的，所以赋值-such-that语句引起了一个证明义务，证明这样的m存在。这个证明义务来自于我们上面断言的属性。

差不多了。为了建立引理的后置条件，我们剩下的计划就是构造一个严格大于Fib(m)的斐波那契数。我们观察到Fib(m) + Fib(m+1)严格大于Fib(m)，因此我们有Fib(m+2)严格大于Fib(m)。

好吧，我们直说了吧。也许我们并没有“观察”到这一点，而是“希望”、“猜想”或“松散地认为”它可能成立。好吧，确实如此。(唷!)我们可以通过询问验证者它是否能为我们证明来验证:

assert k <= Fib(m) + Fib(m + 1) == Fib(m + 2);
1

验证者立即证明了这个断言。4 (opens new window)此外，通过写下这个断言，我们也向验证者展示了见证m+2，它证明了引理的后置条件中的存在量词。

我用这个例子来说明的重点是，你可以用Skolemize一个量词

exists x :: P
1

通过assign-such-that语句

var x :| P;
1

注意标点符号的区别。

# 带外参数的引理

我刚刚给你们看了一个涉及存在量词的例子。这个例子表明，“EverBigger”引理的“证明”两次使用了存在性介绍(在简单情况下为Fib(k)，在困难情况下为Fib(m+2))，从而将“我们手中”的k和m+2转换为存在性量化。这个例子还展示了(递归调用)引理的调用使用存在消除来将引理的后置条件中的存在量化转换为“我们手中的”一个m。让人印象深刻的是，Dafny有这样的特性，它还有一个更有用的特性，可以让你在一开始就避免这些存在-量词转换:引理-参数。

在数学中，引理是由它们所提到的变量参数化的。这些都是参数。一个数学引理很少或永远不会被认为具有外参数。在Dafny中，引理实际上就是一个幽灵方法，一个方法可以同时具有输入参数和输出参数。这是非常有用的。与其用引理来证明某个值的“存在”，还不如直接“返回”某个这样的值。

下面是上面的“EverBigger”引理，但将n声明为out形参:

lemma EverBigger(k: nat) returns (n: nat)
  ensures k <= Fib(n)
{
  if k < 2 {
    n := k;
  } else {
    var m := EverBigger(k-1);
    n := m + 2;
  }
}
1
2
3
4
5
6
7
8
9
10

# 绑定警卫

Dafny还包含了另一个特性，使量词的使用更加流畅:带有*binding guard *的if语句。这样的语句回答了“如果有一个，给我一个在我手里”的命令。

假设我们写一个证明，根据y是否为斐波那契数分成两种情况。然后我们可以这样写:

if exists n :: y == Fib(n) {
  var n :| y == Fib(n);
  // y is the nth Fibonacci number
} else {
  // y is not a Fibonacci number
}
1
2
3
4
5
6

这表达了我们想要的，但感觉有点笨拙，因为我们重复了条件y == Fib(n)。我们可以将这个“if”语句写成

if n :| y == Fib(n) {
  // y is the nth Fibonacci number
} else {
  // y is not a Fibonacci number
}
1
2
3
4
5

:|与赋值such-that语句中的标点相同，而不是存在量词中类似位置的::。

# 集合和映射

逻辑量词和其他结构引入了一些绑定变量，并以某种方式限制了这些绑定变量的取值范围。集合理解和映射理解也是如此。

# 集合理解

很容易在Dafny写下一组。例如,

{ 2, 3, 5 }
1

是三个最小素数的集合。这样的表达式，其中集合的元素被显式列出，称为set display。但是，如果您想要定义的集合不能写成集合显示，该怎么办?

集合理解以图解的方式定义了一组元素。在普通数学符号中集合理解的一个例子是

定义了最小的100个自然数的集合。另一个例子是

它定义了100个最小的完全平方数。这两个推导式中的绑定变量都是，指定range的值由谓词定义。让范围超过这些值，第一个集合然后包含表单的元素，而第二个集合包含表单的元素。也就是说，在第一个集合中，元素是自身的合法值，而在第二个集合中，元素是每个合法值的平方。

更一般地说，数学符号的形状是这样的。读者应该理解这是绑定变量。理解为绑定变量，我们可以通过精确描述集合何时包含一个元素来定义集合推导式:

或者，使用存在函数的取值范围单独给出的符号:

在Dafny中，同样的集合理解有如下形式:

set x | R :: f(x)
1

x是绑定变量(或者，更普遍地说，一个绑定变量的列表)，R是绑定变量的范围谓词，而f(x)是集合推导的项表达式。绑定变量被显式列出，不像普通的数学符号，读者必须推断绑定变量是什么。上面给出的两个示例集在Dafny中写如下:

set x | 0 <= x < 100 :: x
set x | 0 <= x < 100 :: x*x
1
2

虽然乍一看不太简洁，但显式列出绑定变量的表示法有一些细微之处。

一个细微之处是，就像上面一样，量词的定义显示了符号的相似性:

y in (set x | R :: f(x))   <==>   exists x | R :: y == f(x)
1

另一个优点是可以很容易地列出附加的绑定变量。假设R是x和z的谓词，那么这里有两个例子:

set x,n | Fib(n) <= x < Fib(n) + n :: f(x)
set x,n | Fib(n) <= x < Fib(n) + n :: g(x,n)
1
2

第一个集合包含f(x)对于每个在n范围内的x对于某些n的Fib(n)。用普通的数学符号来表示它的一种等价的方式是:

第二个集合包含g(x,n)对于每个x和n，使x在Fib(n)的n之内。在这里，等效的数学符号更笨拙，需要使用另一个绑定变量:

Dafny使绑定变量显式的一般表示法也被许多作者使用(例如，[3 (opens new window)， 4 (opens new window)])。它也类似于其他语言中使用的列表理解表示法。例如，Dafny系列

set x,y | 0 <= x <= y <= 100 && x + y == 100 :: (x,y)
1

它包含一对自然数之和为100，包含与Python列表相同的元素:

[(x,y) for x in range(0, 101) for y in range(x, 101) if x + y == 100]
1

Haskell名单:

[(x,y) | x <- [0..100], y <- [x..100], x + y = 100]
1

# 简化的集合理解

我刚刚花了很多文字来描述Dafny中的一般集合理解符号。然而，在实践中的许多集合推导中，只有一个约束变量，而术语表达式就是那个约束变量。例如，我们已经看到，最小的“100”自然数的集合是:

set x | 0 <= x < 100 :: x
1

对于这种常见的情况，Dafny允许你省略术语表达式，只需要写:

set x | 0 <= x < 100
1

这个表达式看起来像普通的数学符号。事实上，对于这些简化的集合推导式，很容易“理解”数学符号想要表达的约束变量是什么。

作为Dafny中验证器的一个注释，自动化倾向于更好地工作于简化的集合推导式，其中术语表达式可以被省略。

# 映射理解

一个map本质上是一组对，其中对的左元素是唯一的(也就是说，每个左元素在功能上决定了相应的右元素)。与集合的显示表达式一样，map可以通过map display来定义。例如,

map[2 := `c`, 137 := `a`]
1

将整数2映射到字符c，将整数137映射到字符a。每一对像2:= c可以被称为一个maplet。此外，maplet的左元素称为a key，右元素获得不可描述的名称value。

与集合的理解一样，映射可以通过map理解来定义。它的形式是:

map x | R :: f(x) := g(x)
1

例如，

map x | 0 <= x < 100 :: x*x := x
1

是从前100个完全平方数到它们各自的平方根的映射。

如果您将映射理解理解为一组具有唯一键的maplets，那么您基本上已经理解了符号。不过，我将提供一些注释并指出映射特有的一些特性。

需要注意的一点是，maplets必须具有唯一的键。例如，验证者会抱怨，如果你试着写一个像这样的映射理解

map x | -10 <= x <= 10 :: x*x := x
1

因为它说把4映射到2和-2上，这是没用的。

一般的映射理解表达是相当灵活的。例如，假设m是一个从数字到字符的映射，并假设我们想要创建一个新的映射n，从m中的键的子集到其他一些字符。更准确地说，当m中的键在函数f的图像中，比如一个键f(x)对于某个x，然后我们想让n将这个键映射到h(x)。然后我们将n定义为

map x | f(x) in m.Keys :: f(x) := h(x)
1

然而，大多数时候，我们倾向于写的映射理解具有这种形式

map x | R :: x := g(x)
1

对于这些常见的映射，Dafny允许我们省略“x:=”，只写

map x | R :: g(x)
1

在实践中，几乎所有的映射理解都可以用这种简化的形式来写。但是当简化形式不充分时(就像上面的maplets f(x):= h(x)的例子一样)，一般形式是可用的。

# Lambda expressions

最后，要注意映射和函数之间的区别。您可以将map看作是一个预先计算好的表，而函数则是从一个给定的键中计算出一个值。为了进行比较，让我们考虑编写映射

map x | R :: g(x)
1

作为一个函数。

通常，函数是用名称声明的。上面的映射是沿着线写的

function F(x: X): Y
  requires R
{
  g(x)
}
1
2
3
4
5

函数也可以是匿名的，在这种情况下，它通常被称为lambda表达式。然后编写示例映射

x requires R => g(x)
1

# 总结

以下是本文中讨论的语法形式:

forall x :: P
forall x | R :: P
forall x | R ensures P { S; }
exists x :: P
exists x | R :: P
var x :| P;
if x :| P { S; }
set x | R :: f(x)
set x | R
map x | R :: f(x) := h(x)
map x | R :: g(x)
function F(x: X): Y { g(x) }
x requires R => g(x)
1
2
3
4
5
6
7
8
9
10
11
12
13

# 致谢

我很感谢Jay Lorch在这张便条上的许多有帮助的评论。

# 参考文献

[0]Nada Amin, K. Rustan M. Leino, and Tiark Rompf. Computing with an SMT solver. In Martina Seidl and Nikolai Tillmann, editors, Tests and Proofs — 8th International Conference, TAP 2014, volume 8570 of Lecture Notes in Computer Science, pages 20–35. Springer, July 2014. 🔎 (opens new window)

[1]François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53–64, Wrocław, Poland, August 2011. https://hal.inria.fr/hal-00790310 (opens new window). 🔎 (opens new window)

[2]K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988. 🔎 (opens new window)

[3]Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976. 🔎 (opens new window)

[4]David Gries and Fred B. Schneider. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag, 1994. 🔎 (opens new window)

[5]Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A notation for detailed design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175–188. Kluwer Academic Publishers, 1999. 🔎 (opens new window)

[6]K. Rustan M. Leino and Clément Pit-Claudel. Trigger selection strategies to stabilize program verifiers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 361–381. Springer, 2016. 🔎 (opens new window)

0.用于Dafny排版的Emacs IDE某些Dafny结构的符号你更可能在论文中看到。默认情况下，它显示forall x:: P as和显示exists x:: P as。[↩](http://leino.science/papers/krml267.html # back-fn-fn-emacs)

1.在内部，Dafny验证器可以更有效地使用某些量词。验证者试图检测一个给定量词的另一种形式何时可能执行得更好，并将在这些情况下自动重写量词[6 (opens new window)]。例如，它可以选择解除某些量词的嵌套。这种重写的目标是在获得良好的验证性能的同时支持自然外观的程序。[↩](http://leino.science/papers/krml267.html # back-fn-fn-nested)

2.事实证明，Dafny的自动归纳将自动证明FibProperty和FibPropertyAll。如果这是我们唯一关心的引理，那就没有什么好说或做的了。尽管如此，我还是用这个例子来展示“forall”语句。如果你想要确保我将要说的是一个证明，你可以通过使用属性{:induction false}来关闭FibPropertyAll的自动感应。[↩](http://leino.science/papers/krml267.html # back-fn-fn-fibpropertyall)

3.Dafny也可以证明类似断言assert Fib(12) == 144;。在内部，Dafny使用了函数的“双轨编码”，使其能够获得Fib(12)的值(因为12是一个文字常量)和Fib(k)(其中k是一个变量)。如果您对这是如何实现的感兴趣，我建议您访问[0 (opens new window)]。[↩](http://leino.science/papers/krml267.html # back-fn-fn-dual-rail-encoding)

4.这里是断言k <= Fib(m) + Fib(m+1)的一个证明。在我们的证明中，“困难的情况”适用于当k至少为2时，所以k-1至少为1，所以我们知道Fib(m)至少为1。由此可以得出结论，对于Fib(0) == 0， m不能为0。这很重要，因为这意味着m+1至少等于2，因此适用于Fib定义的归纳情况。换句话说，我们有Fib(m+1) == Fib(m) + Fib(m-1)。我们已经得出，Fib(m)至少等于1。以Fib返回nat为例，我们知道Fib(m-1)至少为0。所以，Fib(m+1)至少等于1。换句话说，Fib(m) + Fib(m+1)至少比Fib(m)大于1，而Fib(m)至少等于k-1。因此，Fib(m) + Fib(m+1)至少等于k。

如果我们把“简单的情况”和“困难的情况”分开，使“简单的情况”只包含“k == 0”，那么我们不可能在上面的论证中得出“m != 0”的结论。其他交互式证明助手的一些用户可能会对此感到困扰，因为他们会说k具有nat类型，因此对k的归纳应该使用k == 0作为基本情况。数学对归纳法没有这样的限制，事实上，正如这个证明所显示的，我们可以从将“EverBigger”的情况分成“k < 2”和“2 <= k”中获益。[↩](http://leino.science/papers/krml267.html # back-fn-fn-proof)

编辑 (opens new window)
上次更新: 2022/03/26, 14:38:56
定义、证明、算法正确性的案例研究GCD
不同类型的证明

← 不同类型的证明→

最近更新
01
寻找最大和最小数
04-06
02
斐波那契数列
04-06
03
线性查询
04-06
更多文章>
Theme by Vdoing | Copyright © 2022-2022 Li Jiahai | Dafny Community | 2022