Dafny Dafny
首页
  • 入门介绍

    • 什么是dafny?
  • 用起来吧!

    • 安装
    • 快速上手
    • 可能遇到的问题?
  • Dafny快速入门

    • 基础学习 Basic
    • 方法 Method
    • 关键字 Keyword
    • 函数 Function
    • 类 Class
    • 泛型 Generics
    • 声明 Statement
    • 表达式 Expression
  • Dafny简单例子

    • 寻找最大最小数和
    • 斐波那契数列
    • 线性查询
    • 引理-计算序列非负元素个数
    • 集合
    • 终止
  • Dafny指导

    • 介绍
    • 方法 Methods
    • 前置/后置条件 Pre/Postconditions
    • 断言 Assertions
    • 函数 Functions
    • 循环不变体 Loop Invariants
    • 数组 Arrays
    • 量词(函数) Quantifiers
    • 谓词(函数) Predicates
    • 框架 Framing
    • 二分搜索 Binary Search
    • 总结
  • Dafny进阶语法

    • 引理和归纳 Lemmas and Induction
    • 模块 Modules
    • 集合 sets
    • 序列 sequence
    • 终止 Terminal
    • 值类型 Values Types
  • 实践探索

    • 自动归纳
    • 自动调用引理
    • 定义、证明、算法正确性
    • 各种推导式
    • 不同类型的证明
    • 集合元素上的函数
    • 在集合上的迭代
  • 常用工具

    • Type System
    • Style Guide
    • Cheet Sheet
✨收藏
  • 简体中文
  • English
💬社区留言板
GitHub (opens new window)

Dafny

新一代验证语言
首页
  • 入门介绍

    • 什么是dafny?
  • 用起来吧!

    • 安装
    • 快速上手
    • 可能遇到的问题?
  • Dafny快速入门

    • 基础学习 Basic
    • 方法 Method
    • 关键字 Keyword
    • 函数 Function
    • 类 Class
    • 泛型 Generics
    • 声明 Statement
    • 表达式 Expression
  • Dafny简单例子

    • 寻找最大最小数和
    • 斐波那契数列
    • 线性查询
    • 引理-计算序列非负元素个数
    • 集合
    • 终止
  • Dafny指导

    • 介绍
    • 方法 Methods
    • 前置/后置条件 Pre/Postconditions
    • 断言 Assertions
    • 函数 Functions
    • 循环不变体 Loop Invariants
    • 数组 Arrays
    • 量词(函数) Quantifiers
    • 谓词(函数) Predicates
    • 框架 Framing
    • 二分搜索 Binary Search
    • 总结
  • Dafny进阶语法

    • 引理和归纳 Lemmas and Induction
    • 模块 Modules
    • 集合 sets
    • 序列 sequence
    • 终止 Terminal
    • 值类型 Values Types
  • 实践探索

    • 自动归纳
    • 自动调用引理
    • 定义、证明、算法正确性
    • 各种推导式
    • 不同类型的证明
    • 集合元素上的函数
    • 在集合上的迭代
  • 常用工具

    • Type System
    • Style Guide
    • Cheet Sheet
✨收藏
  • 简体中文
  • English
💬社区留言板
GitHub (opens new window)
  • dafny-quick-start

  • dafny-tutorials

  • detailed-document

  • publication-lecture

    • Automatic Induction
    • Calling Lemmas Automatically
      • Case study of definitions, proofs, algorithm correctness GCD
      • Comprehensions
      • Different Styles of Proofs
      • Functions over Set Elements
      • Iterating over a Collection
      • old and unchanged
      • Short-Circuit Operators
      • Statement versus Expression Syntax
      • The Parent Trick for proving termination and a function-by-method use case
      • Type-Parameter Completion
      • Type-parameter modes variance and cardinality preservation
    • 语言
    • publication-lecture
    lijiahai
    2022-03-26
    目录

    Calling Lemmas Automatically

    Dafny Power User: Calling Lemmas Automatically

    K. Rustan M. Leino

    Manuscript KRML 265, 8 June 2019

    Abstract. Some properties of a function are more useful than others. If you have proved such a property as a lemma, you may want to have it be applied automatically. This note considers ways to achieve something like that in Dafny.

    On https://github.com/Microsoft/dafny/issues/231 (opens new window), a Dafny user asked:

    Is there a way in Dafny to mark a lemma as “automatic” and add it to the knowledge base of z3 ?

    For student homeworks, we often stumble on specifications that are just a bit too complex for Dafny to prove, and require some hand-crafted asserts or lemmas.

    It would be nice if we could define those lemmas to augment boogie/z3 search space with domain-specific knowledge, avoiding the need to explain to our students how lemmas work, and the tedious and difficult task to find and use the required lemmas.

    Is something like an {:auto} annotation feasible ? Can we augment the .bpl axiomatization ?

    Here is an example that shows the issue. Suppose you declare a function and prove a property about it:

    function FibFib(n: nat): nat {
      if n == 0 then 0
      else if n == 1 then 2
      else FibFib(n-2) + FibFib(n-1)
    }
    
    lemma FibFibIsEven(n: nat)
      ensures FibFib(n) % 2 == 0
    {
      // automatically proved by induction
    }
    
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11

    For your application, it may be crucial that FibFib always returns an even number. Using the declarations above, you would then have to call the lemma FibFibIsEven every time you use the function. This is tedious. Is there some way to instruct Dafny to automatically apply FibFibIsEven whenever it's needed?

    No, there's no such feature in Dafny. (VCC had such a feature, for example.) In some situations, such automation may work well. In other situations, it may cause the lemma to be invoked too many times (say, an infinite number of times), which is problematic.

    If you have an interest in trying out some kind of {:autoLemma} feature, please feel free to play around with the open Dafny sources. In the present state, I have four suggestions that you may try, and which may alleviate some of the tedium you're experiencing.

    # Uber Lemmas

    One suggestion is to create an “uber lemma” that collects the statements of several other lemmas. For example, if you already have:

    lemma Lemma0(x: X) ensures P0(x) { ... }
    lemma Lemma1(x: X) ensures P1(x) { ... }
    lemma Lemma2(x: X) ensures P2(x) { ... }
    
    1
    2
    3

    then you can combine them into one:

    lemma Everything(x: X)
      ensures P0(x) && P1(x) && P2(x)
    {
      Lemma0(x: X);
      Lemma1(x: X);
      Lemma2(x: X);
    }
    
    1
    2
    3
    4
    5
    6
    7

    This lets you get all 3 properties by calling a single lemma.

    # Aggregate Lemma Invocations

    Another suggestion is to invoke a lemma on many values at the same time. Given:

    lemma LemmaForOneX(x: X) ensures P(x) { ... }
    
    1

    you can invoke this lemma for all values of X simultaneously:

    forall x {
      LemmaForOneX(x);
    }
    
    1
    2
    3

    By placing this forall statement at the beginning of some code you're trying to prove, you have in effect called it for every imaginable value of X. You can of course also tuck this statement into a lemma of its own and then call this one lemma:

    lemma LemmaForEveryX()
      ensures forall x :: P(x)
    {
      forall x {
        LemmaForOneX(x);
      }
    }
    
    1
    2
    3
    4
    5
    6
    7

    In many cases, this will work fine. In other cases, the verifier may not realize that you have called the lemma on the value that needs the individual lemma, so you may still need to invoke LemmaForOneX manually. Also, Dafny takes measure to avoid “matching loops” in the quantifiers generated for the lemma calls above (“matching loops” are what can cause an infinite number of uses of the lemmas). However, the mechanism is not perfect, so this added automation may in some cases cause degraded performance.

    # Function Postconditions

    A third suggestion is to declare some of the most useful properties of a function in the postcondition of the function, rather than in a separate lemma. For example, instead of:

    function F(x: X): int { ... }
    lemma AboutF(x: X)
      ensures F(x) % 2 == 0
    { ... }
    
    1
    2
    3
    4

    you can declare:

    function F(x: X): int
      ensures F(x) % 2 == 0
    { ... }
    
    1
    2
    3

    To obtain the property stated by the lemma, you must call the lemma. In contrast, any property stated in the postcondition of a function is automatically applied every time you call the function.

    As I've mentioned, more information can help the verifier do more things automatically, but too much information can also overwhelm and confuse the verifier. Therefore, my suggestion is to use function postconditions only for those properties that you think every user of the function will need. Properties needed more rarely are better off declared in lemmas that have to be manually invoked.

    Also, there are limits to what you can write in a function postcondition. In particular, what you write must “terminate”. In practice, this means you may have problems mentioning the function applied to other arguments in the postcondition. For example,

    predicate R(x: X, y: X)
      // commutativity:
      ensures R(x, y) <==> R(y, x)
      // transitivity:
      ensures forall z :: R(x, z) && R(z, y) ==> R(x, y)
    
    1
    2
    3
    4
    5

    is not admitted, because there are self-referential non-terminating (that is, infinitely recursive) calls in the postcondition. Thus, properties like commutativity and transitivity always need to be stated as separate lemmas.

    # Basic/premium function pairs

    A function postcondition conveniently provides all users of a function with the property that it states, alleviating the need to call the lemma explicitly. If the property is not interesting for all users, a fourth suggestion is to declare two functions. The basic function gives the actual definition of the function and an accompanying lemma states the property about it. The premium function calls the basic function and states the property as its postcondition, which is proved by a call to the lemma.

    function F(x: X): int { ... }
    lemma AboutF(x: X)
      ensures F(x) % 2 == 0
    { ... }
    
    function F_premium(x: X): int
      ensures F_premium(x) % 2 == 0
    { AboutF(x); F(x) }
    
    1
    2
    3
    4
    5
    6
    7
    8

    Users can now choose: a call to F_premium obtains both the value of the function and the proved property, whereas a call to F obtains only the value. If you expect the premium version to be more popular than the basic version, you can of course rename F and F_premium to F_basic and F, respectively.

    Other than the postcondition, the two functions are synonyms. Semantically. A note of caution is that the mechanism the verifier uses as a guide to its use of quantifiers is syntactic. Therefore, which of the two functions you use in the body of a quantifier can make a difference in when the verifier decides to instantiate the quantifier. For this reason, I suggest you use the basic version of the function inside any quantifier you write.

    # Acknowledgments

    Bryan Parno provided the fourth suggestion of wrapping a basic version of a function and its lemma into a premium version of the function.

    编辑 (opens new window)
    上次更新: 2022/03/26, 14:38:56
    Automatic Induction
    Case study of definitions, proofs, algorithm correctness GCD

    ← Automatic Induction Case study of definitions, proofs, algorithm correctness GCD→

    最近更新
    01
    寻找最大和最小数
    04-06
    02
    斐波那契数列
    04-06
    03
    线性查询
    04-06
    更多文章>
    Theme by Vdoing | Copyright © 2022-2022 Li Jiahai | Dafny Community | 2022
    • 跟随系统
    • 浅色模式
    • 深色模式
    • 阅读模式