程序验证之Dafny--证明霍尔逻辑的半自动化利器

                                     一、What is Dafny?【来自官网介绍 Dafny 

1)介绍

Dafny 是一种支持验证的编程语言,配备了一个静态程序验证器。

通过将复杂的自动推理与熟悉的编程习语和工具相结合,使开发者能够编写可证明正确的代码(相对于 {P}S{Q} 这种霍尔三元组的规范而言)。

Dafny 还可以将 Dafny 代码编译到熟悉的开发环境,如 C#、Java、JavaScript、Go 和 Python;使得严格的验证成为开发过程的有机组成部分,从而减少了可能在测试中被遗漏的、代价高昂的后期错误。

2)原理

Dafny验证器根据我们提供的前置条件后置条件,以及循环不变式,自动生成验证条件(Verification Condition,VC)的逻辑公式。 这些验证条件主要包含,不变式的可达性归纳性,以及使用循环不变式证明后置条件。 这些逻辑公式都会交给同样是由微软开发的SMT求解器Z3来求解,并依据求解结果,返回验证结果。

二、使用快速入门:


2.1 一个.dfy后缀的文件:

程序主要包含以下几部分:

  1. 类型(types)

  2. 方法(methods)

  3. 函数(functions)

  4. 用户自定义的类型包括类(class)和归纳数据类型(inductive class)

  5. 类class本身也包含一组声明(declarations)、介绍字段(introducing fields)、方法(methods)和函数(functions)

注释:// 双斜杠 或者 /* xxxxx */

2.1.1基本定义

在类中,定义字段x为数据类型(types)T: var x: T

注意事项:

  • 数据类型必需手动申明的,不会被自动推断。

  • 通过在声明前加上关键 ghost 可以将该字段声明为幽灵(即用于规范而不是执行)字段。

Dafny 的9种数据类型包括:

  • bool:布尔值
  • int:无界整数
  • string: 字符串
  • class/inductive class: 用户自定义的类和归纳类、
  • set<T>:不可变的无序集合
  • seq<T>:不可变的有序集合
  • array<T>array2<T>array3<T>: 多维数组类型
  • object:所有类型的超类
  • nat:范围是int一半,非负整数。

2.1.2方法 methods

方法的声明如下:

method M(a: A, b: B, c: C) r eturns (x: X, y: Y, z: Y)  //输入输出参数
requires Pre	//前置条件
modifies Frame  //框架
ensures Post	//后置条件
decreases TerminationMetric //变体函数
{
Body //函数体`
}

其中:

  • a, b, c : 输入参数
  • x, y, z : 输出参数
  • Pre: 表示方法 前提条件 的 布尔表达式
  • Frame: 表示类对象的集合,可以被方法更新(Frame denotes a set of objects whose fields may be updated by the method)
  • Post: 是方法 后置条件 的 布尔表达式
  • TerminationMetric: 是方法的变体函数(TerminationMetric is the method’s variant function)
  • Body: 是实现方法的语句。

2.1.2.1框架Frame

框架Frame 是单个或多个对象组成的表达式的集合。(见下面例子)

框架Frame是由类内对象和类外方法内对象两部分组成。(反正就是一堆类对象的集合)

例如,如果 c 和 d 是类C的对象,那么以下每行意思是一样的。

  • modifies {c, d}

  • modifies {c} + {d}

  • modifies c, {d}

  • modifies c, d

如果方法内啥都没写,那么前置和后置条件默认为真,框架默认为空集。

2.1.2.2变体函数 variant function

变体函数是一个表达式组成的列表,表示由给定表达式组成的字典元组,后跟隐含的“top”元素。

如果省略没写的话,Dafny 将猜测该方法的变体函数,通常是以该方法的参数列表开头的字典元组。

Dafny IDE 将在工具提示中显示猜测。

2.1.2.3ghost 关键字

通过在声明之前加上关键字 ghost 可以将方法声明为 ghost方法(仅规范而不用于执行)。

2.1.2.4this 关键字

默认情况下,类中的方法都具有隐式接收器参数 this。可以通过在方法声明之前使用关键字 static 来删除此参数。

类 C 中的静态方法 M 可以由 C.M(...) 调用。

2.1.2.5构造函数/构造体 constructor

在类中,一个方法可以通过将method关键字替换为constructor,申明一个构造方法。

构造函数(构造方法)只能在分配对象时调用(参见示例)

对于包含一个或多个构造函数的类,对象创建必须与对构造函数的调用一起完成。

通常,一个方法当然得有一个名字,但是一个类可以有一个没有名字的构造函数,也就是匿名构造函数 constructor (n:int )

constructor (n: int) //constructor 匿名构造器` 
modifies this //框架内对象的构造体 this就是this.frame?`{Body
}

2.1.3函数 function

函数具有以下形式:

function F(a: A, b: B, c: C): T
requires Pre  //前置条件pre
reads Frame	//框架frame
ensures Post //后置条件post
decreases TerminationMetric //变体函数
{Body	//函数体
}
  • abc : 输入的形参,
  • T : 返回结果的类型,
  • Pre: 表示函数前提条件的布尔表达式,
  • Frame: 函数体body需要的对象列表
  • Post: 函数的后置条件布尔表达式
  • TerminationMetric: 变体函数
  • Body: 定义函数的表达式。

前置条件允许函数是部分的(只用前置就行不用写后置),即前置条件表示函数何时定义,并且 Dafny 会验证函数的每次使用都满足前置条件。

通常不需要后置条件,因为函数在函数体内已经给出了完整的定义。

例如:

(写个后置加个保险也行,一般后置就是声明该函数的基本属性,比如Factorial这个函数所有数字都≥1)

function Factorial(n: int): int
requires 0 <= n //前置条件pre
ensures 1 <= Factorial(n) //后置条件post
{if n == 0 then 1 else Factorial(n-1) * n //函数体body
}

要在后置条件中引用函数的结果,请使用函数本身的名称,如示例中所示。

默认情况下,函数是ghost,不能从可执行(非ghost)代码中调用。

为了使它从ghost变成非ghost,用关键字function method替换 function.

一个返回布尔值的函数可以用关键字声明,然后省略冒号和返回类型。

如果函数或方法被声明为类class成员,则它具有隐式接收器参数 this。可以通过在声明之前加上关键字static来删除此参数。

类 C 中的静态函数 F 可以被 C.F(...) 调用。

E.g.2:[educoder实训实例]:

method test(n: int) returns (sum: int)requires n >= 0ensures sum * 2 == n * (n+1)
{sum := 0;var i:int := 0;while i <= ninvariant i<=n+1invariant sum*2 == i*(i-1){sum := sum + i;i := i + 1;}
}

2.1.3.1 类 class

一个类定义如下:

class C {// member declarations go here
}

其中类的成员(字段、方法和函数)在花括号内定义(如上所述)。

2.1.3.2数据类型 datatypes

归纳数据类型(inductive datatype)是一种类型,其值是用一组固定的构造函数创建的。

数据类型 为Tree带有构造函数 Leaf 和 Node 的函数声明如下:

datatype Tree = Leaf | Node(Tree, int, Tree)//Leaf为无参构造函数 Node为有参

构造函数由竖线分隔。 无参数构造函数不需要使用括号,如 Leaf 所示。

对于每个构造函数 Ct,数据类型隐式声明了一个布尔成员 Ct?,对于已经使用 Ct 构造函数赋的值的成员,它返回 true。 例如,在代码片段之后:

var t0 := Leaf; var t1 := Node(t0, 5, t0);

表达式 t1.Node结果为 true, t0.Node结果为false。

如果两个数据类型值是使用相同的构造函数和该构造函数的相同参数创建的,则它们是相等的。因此,对于像 Leaft.Leaf 这样的无参数构造函数,Dafny会给出与 t == Leaf 相同的结果。(没看懂,不管了)

构造函数可以选择为其任何参数声明析构函数,这是通过为参数引入名称来完成的。 例如,如果 Tree 被声明为:

datatype Tree = Leaf | Node(left: Tree, data: int, right: Tree)

那么t1.data == 5t1.left == t0在上面的代码片段之后保持不变。(还是没懂)

2.1.3.3泛型 Generics

Dafny同其他语言一样都有泛型,任何类、方法、函数都可以有类型参数,在<>中申明该数据类型T

class MyMultiset<T> {/*...*/
}		//类泛型
datatype Tree<T> = Leaf | Node(Tree<T>, T, Tree<T>) //自定义数据泛型
method Find<T>(key: T, collection: Tree<T>) { //方法泛型`/*...*/
}function IfThenElse<T>(b: bool, x: T, y: T): T {	//函数泛型/*...*/
}

2.1.3.4声明 Statement

以下是 Dafny 中最常见语句:

var LocalVariables := ExprList;
Lvalues := ExprList;
assert BoolExpr;
print ExprList;if BoolExpr0 {Stmts0
} else if BoolExpr1 {Stmts1
} else {Stmts2
}while BoolExprinvariant Invmodifies Framedecreases Rank
{Stmts
}match Expr {case Empty => Stmts0case Node(l, d, r) => Stmts1
}break;return;
函数/方法的返回值赋值给变量

(就是将函数/方法返回的值或对象 赋给 一个局部变量而已) var LocalVariables := ExprList; var 语句引入了局部变量。 Lvalues := ExprList;

赋值语句将 ExprList变量赋给Lvalues。 这些分配是并行执行的(更重要的是,所有必要的读取都发生在写入之前),因此左侧必须表示不同的 L 值。 每个右侧都可以是以下形式之一的表达式或对象创建:

  1. new T

  2. new T.Init(ExprList)

  3. new T(ExprList)

  4. new T[SizeExpr]

  5. new T[SizeExpr0, SizeExpr1]

第一种形式分配一个类型为 T 的对象。

第二种形式另外在新分配的对象上调用初始化方法或构造函数。

第三种形式是当调用匿名构造函数时的语法。

其他形式分别了T是一维和二维数组对象的匿名构造方法

assert 声明

assert 语句判断后面的表达式结果是否为真(由验证器验证)。

打印语句将给定打印表达式的值输出到标准输出。字符串中的字符可以转义;例如,对 print 语句感兴趣的是 \n 表示字符串中的换行符。

if 选择语句

if 语句是通常的语句。该示例显示了使用 else if 将备选方案串在一起。像往常一样,else 分支是可选的。

while 循环语句
  • while 语句是通常的循环,其中
  • invariant 声明给出了一个循环变量
  • modifies语句限制了循环的框架
  • reduction语句从循环中引入了一个变体函数。

默认情况下,循环不变式为真,修改框与封闭上下文中的相同(通常是封闭方法的修改子句),并从循环保护中猜测变体函数。(真没看懂)

while BoolExpr //布尔表达式-循环条件`invariant Invmodifies Framedecreases Rank{Statements
}
break语句

break 语句可用于退出循环,而 return 语句可用于退出方法。

2.1.4 表达式 Expressions

Dafny 中的表达式与类 Java 语言中的表达式非常相似。以下是一些值得注意的差异。

2.1.4.1基本运算符

除了短路布尔运算符 && (and) 和 || (或),Dafny 有一个短路蕴涵运算符 ==> 和一个 if-and-only-if 运算符 <==>

正如它们的宽度所暗示的那样,<==> 具有比 ==>低的绑定力,而后者又比 && 和 ||具有更低的绑定力。

Dafny 比较表达式可以是链式的,这意味着相同方向的比较可以串在一起。例如,

0 <= i < j <= a.Length == N

含义相同: 

0 <= i && i < j && j <= a.Length && a.Length == N

请注意,布尔相等可以使用 == 和 <==> 来表示。这些之间有两个区别。首先,== 比 <==> 具有更高的约束力。其次,== 是链接,而 <==> 是关联的。也就是说,a == b == c 与 a == b && b == c 相同,而 a <==> b <==> c 与 a <==> (b <== > c),这也与 (a <==> b) <==> c 相同。

整数运算

对整数的运算是常用的运算,除了 /(整数除法)和 %(整数模)遵循欧几里德定义,这意味着 % 总是导致非负数。 (因此,当 / 或 % 的第一个参数为负数时,结果与您在 C、Java 或 C# 中得到的结果不同,请参阅 http://en.wikipedia.org/wiki/Modulo_operation。)

集合运算

集合上的操作包括+(并)、*(交)和-(集合差)、集合比较运算符<(真子集)、<=(子集)、它们的对偶> 和>=,以及!! (脱节)。 S 中的表达式 x 表示 x 是集合 S 的成员,而 x !in S 是一个方便的写法 !(x in S)

要从某些元素创建一个集合,请将它们括在花括号中。例如,{x,y} 是由 x 和 y 组成的集合(如果 x == y,则为单例集),{x} 是包含 x 的单例集,{} 是空集。

序列运算

对序列的操作包括 +(连接)和比较运算符 <(适当的前缀)和 <=(前缀)。成员资格可以像集合一样检查:x in S 和 x !in S。序列 S 的长度表示为 |S|,并且此类序列的元素具有从 0 到小于 |S| 的索引。表达式 S[j] 表示序列 S 的索引 j 处的元素。表达式 S[m..n],其中 0 <= m <= n <= |S|,返回一个序列,其元素是S 从索引 m 开始(即,从 S[m]、S[m+1]、……直到但不包括 S[n])。表达式 S[m..]; (通常称为“drop m”)与 S[m..|S|] 相同;也就是说,它返回除 S 的前 m 个元素之外的所有元素的序列。表达式 S[..n] ; (通常称为“take n”)与 S[0..n] 相同,即它返回由 S 的前 n 个元素组成的序列。

如果 j 是序列 S 的有效索引,则表达式 S[j := x];是类似于 S 的序列,只是它在索引 j 处有 x。

最后,要从一些元素组成一个序列,请将它们括在方括号中。例如,[x,y] 是由两个元素 x 和 y 组成的序列,使得 [x,y][0] == x 和 [x,y][1] == y,[x] 是唯一元素是 x 的单例序列,[] 是空序列。

if-then-else判断语句

if-then-else 表达式的形式为:if BoolExpr then Expr0 else Expr1

其中 Expr0 和 Expr1 是相同类型的任何表达式。与 if 语句不同,if-then-else 表达式使用 then 关键字,并且必须包含显式的 else 分支。

三、环境配置及实例

vscode内配置dafny:

打开[.dfy]文件:

插件默认在每次执行文件保存操作后,尝试对Dafny代码进行验证。未验证通过的位置会有红色波浪线标出,鼠标在红色波浪线处悬停会显示错误详情。

无法验证显示:

成功显示:

项目首页 - dafny - GitCode

达夫尼博客 |来自 Dafny 维护者和嘉宾的新闻和教育材料。

简单上手 | Dafny (aaron-clou.github.io)https://aaron-clou.github.io/dafnycommunity/pages/39fb20/#hello-dafny

程序验证(5)- 程序验证案例 - 知乎 (zhihu.com)https://zhuanlan.zhihu.com/p/312501103

dafny-lang/dafny: Dafny is a verification-aware programming language (github.com)https://github.com/dafny-lang/dafny

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/bicheng/13037.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

表白成功率百分百的向女朋友表白网页源代码,向女友表白HTML源代码

表白成功率百分百的向女朋友表白网页源代码&#xff0c;向女友表白HTML源代码 效果&#xff1a; 完整代码下载地址&#xff1a;向女友表白HTML源代码 <!DOCTYPE html> <!--STATUS OK--> <html><head><meta http-equiv"Content-Type" c…

性能优化:几方面考虑

我们可以继续再考虑下关于性能优化&#xff0c;我们还能从哪些方面着手呢&#xff1f; 1. 代码层面&#xff1a; 使用更高效的数据结构和算法。使用缓存避免多次数据库交互减少不必要的计算和内存分配。利用并行和异步编程提高性能。使用性能分析工具定位和优化瓶颈。 2. We…

玩转Matlab-Simscape(初级)-01-从一个简单模型开始学习之旅

** 玩转Matlab-Simscape&#xff08;初级&#xff09;- 01 - 从一个简单模型开始学习之旅 ** 目录 玩转Matlab-Simscape&#xff08;初级&#xff09;- 01 - 从一个简单模型开始学习之旅 前言一、从模板开始建模二、建模一个简单的连杆2.1 建模2.2 生成子系统 总结 前言 在产…

代码随想录算法训练营Day40 | 62.不同路径 63. 不同路径 II

代码随想录算法训练营Day40 | 62.不同路径 63. 不同路径 II LeetCode 62.不同路径 题目链接&#xff1a;LeetCode 62.不同路径 思路&#xff1a; 二维数组dp&#xff0c;简单 class Solution { public:int uniquePaths(int m, int n) {if( m1 || n1 ) return 1;vector<v…

2024年成都高新区支持企业申报国家、省级、市级大数据产业发展、新一代信息技术与制造业融合发展、工业互联网推广应用等试点示范项目申报对象条件和奖补

一、申报对象 &#xff08;一&#xff09;本政策支持注册地址、税收关系在成都高新区&#xff0c;具有独立法人资格的企业。 &#xff08;二&#xff09;管理规范&#xff0c;无不良信用记录&#xff0c;自觉遵守安全生产、环境保护等方面的法律法规&#xff0c;近三年未发生…

Git服务器(中心仓库(裸仓库))搭建

目录 前言&#xff1a;Git三大重要的区域 前言&#xff1a;SVN与Git的最主要的区别 搭建Git服务器 git init --bare初始化中心仓库(裸仓库) 前言&#xff1a;Git三大重要的区域 工作区&#xff1a;简单理解就是需要进行版本控制的某个文件夹(假设为test)这个文件夹有一些特…

元类结合__new__

__new__:用来生成骨架 __init__:骨架添加血肉 【一】类中的__new__ class MyClass(object):def __init__(self,name,age):print(f"给当前MyClass类的对象初始化属性的时候会触发__init__")self.name nameself.age age ​def __call__(self,*args,**kwargs):pri…

isinstance和issubclass的使用

isinstance() : 判断当前对象是否是某一个类的类型 issubclass() : 校验一个类是否属于另一个类的子类 class Person(object):... ​ ​ class Student:... ​ ​ stu Student() ​ person Person() ​ # 【一】isinstance() : 判断当前对象是否是某一个类的类型 print(is…

23.HashMap的put方法流程

一、put方法的流程图 二、put方法的执行步骤 首先&#xff0c;根据key值计算哈希值。然后判断table数组是否为空或者数组长度是否为0&#xff0c;是的话则要扩容&#xff0c;resize&#xff08;&#xff09;。接着&#xff0c;根据哈希值计算数组下标。如果这个下标位置为空&a…

第 397 场 LeetCode 周赛题解

A 两个字符串的排列差 模拟&#xff1a;遍历 s s s 记录各字符出现的位置&#xff0c;然后遍历 t t t 计算排列差 class Solution {public:int findPermutationDifference(string s, string t) {int n s.size();vector<int> loc(26);for (int i 0; i < n; i)loc[s…

合并K个升序链表

题目 解法一 优先级队列 思想 将每个链表中的一个节点存放到优先级队列中&#xff0c;本题采用小根堆&#xff0c;将小根堆中的根节点取出&#xff0c;插入到最终的链表中&#xff0c;并且将该节点在原链表中的下一个节点插入小根堆中&#xff08;需要向下调整&#xff09;&a…

【019】基于SSM+JSP实现的进销存管理系统

项目介绍 进销存管理系统是对企业生产经营中物料流、资金流进行条码全程跟踪管理&#xff0c;从接获订单合同开始&#xff0c;进入物料采购、入库、领用到产品完工入库、交货、回收货款、支付原材料款等&#xff0c;每一步都为您提供详尽准确的数据。有效辅助企业解决业务管理…

2024OD机试卷-找座位 (java\python\c++)

题目:找座位 题目描述 在一个大型体育场内举办了一场大型活动,由于疫情防控的需要,要求每位观众的必须间隔至少一个空位才允许落座。 现在给出一排观众座位 分布图 ,座位中存在已落座的观众,请计算出,在不移动现有观众座位的情况下,最多还能坐下多少名观众。 输入描述…

【机器学习】:基于决策树与随机森林对数据分类

机器学习实验报告&#xff1a;决策树与随机森林数据分类 实验背景与目的 在机器学习领域&#xff0c;决策树和随机森林是两种常用的分类算法。决策树以其直观的树形结构和易于理解的特点被广泛应用于分类问题。随机森林则是一种集成学习算法&#xff0c;通过构建多个决策树并…

kafka用java收发消息

用java客户端代码来对kafka收发消息 具体代码如下 package com.cool.interesting.kafka;import org.apache.kafka.clients.consumer.ConsumerConfig; import org.apache.kafka.clients.consumer.ConsumerRecord; import org.apache.kafka.clients.consumer.ConsumerRecords; i…

Microsoft 发布了 5 月份产品安全修复报告。

我们提请大家注意我们归类为趋势*的两个漏洞&#xff1a; CVE-2024-30051 和 CVE-2024-30040。 1. Windows 内核库 DWM 核心库中的 CVE-2024-30051漏洞 该漏洞与负责显示桌面窗口&#xff08;DWM&#xff09;的内核库中的权限升级有关。成功利用漏洞可讓攻擊者在沒有使用者互…

Python模块之Numpy(五)-- 排序

Sort排序 NumPy 的排序方式主要可以概括为直接排序和间接排序两种&#xff0c;直接排序是对数值直接进行排序&#xff0c;间接排序是指根据一个或者多个键对数据集进行排序&#xff0c;在 NumPy 中&#xff0c;直接排序经常使用 sort 函数&#xff0c;间接排序经常使用 argsort…

商品服务:SPUSKU规格参数销售属性

1.Object划分 1.PO&#xff08;Persistant Object&#xff09;持久对象 PO就是对应数据库中某个表中的一条记录&#xff0c;多个记录可以用PO的集合。PO中应该不报含任何对数据库的操作 2.DO(Domain Object) 领域对象 就是从现实世界中抽象出来的有形或无形的业务实体。 3…

mysql字段乱序 information_schema

select COLUMN_NAME from information_schema.columns where table_namecollect_column_info and table_schema nz; 返回ASCII排列 导致 sqoop import \ --connect "jdbc:mysql://your_host/collect" \ --username your_username \ --password your_password \ --t…

SPI通信(使用SPI读写W25Q64)

SPI通信协议 • SPI&#xff08;Serial Peripheral Interface&#xff09;是由Motorola公司开发的一种通用数据总线 • 四根通信线&#xff1a; SCLK:串行时钟线&#xff0c;用来提供时钟信号的。 MOSI:主机输出&#xff0c;从机输入 MISO:从机输出&#xff0c;主机输入 SS:…