c 手机网站开发工具,营销团队,张家港哪家做企业网站,郑州网站制作郑州网站制作案例一、What is Dafny?【来自官网介绍 Dafny 】
1)介绍
Dafny 是一种支持验证的编程语言#xff0c;配备了一个静态程序验证器。
通过将复杂的自动推理与熟悉的编程习语和工具相结合#xff0c;使开发者能够编写可证明正确的代码#xff08;相对于 {P}#xff33;{Q} 这种… 一、What is Dafny?【来自官网介绍 Dafny 】
1)介绍
Dafny 是一种支持验证的编程语言配备了一个静态程序验证器。
通过将复杂的自动推理与熟悉的编程习语和工具相结合使开发者能够编写可证明正确的代码相对于 {P}{Q} 这种霍尔三元组的规范而言。
Dafny 还可以将 Dafny 代码编译到熟悉的开发环境如 C#、Java、JavaScript、Go 和 Python;使得严格的验证成为开发过程的有机组成部分从而减少了可能在测试中被遗漏的、代价高昂的后期错误。
2)原理 Dafny验证器根据我们提供的前置条件后置条件以及循环不变式自动生成验证条件Verification ConditionVC的逻辑公式。 这些验证条件主要包含不变式的可达性归纳性以及使用循环不变式证明后置条件。 这些逻辑公式都会交给同样是由微软开发的SMT求解器Z3来求解并依据求解结果返回验证结果。 二、使用快速入门: 2.1 一个.dfy后缀的文件:
程序主要包含以下几部分 类型(types) 方法(methods) 函数(functions) 用户自定义的类型包括类class和归纳数据类型(inductive class) 类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: 用户自定义的类和归纳类、setT不可变的无序集合seqT不可变的有序集合arrayT、array2T、array3T: 多维数组类型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 //函数体
}a, b, c : 输入的形参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 * (n1)
{sum : 0;var i:int : 0;while i ninvariant in1invariant 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。
如果两个数据类型值是使用相同的构造函数和该构造函数的相同参数创建的则它们是相等的。因此对于像 Leaf、t.Leaf 这样的无参数构造函数Dafny会给出与 t Leaf 相同的结果。(没看懂不管了)
构造函数可以选择为其任何参数声明析构函数这是通过为参数引入名称来完成的。 例如如果 Tree 被声明为 datatype Tree Leaf | Node(left: Tree, data: int, right: Tree) 那么t1.data 5和t1.left t0在上面的代码片段之后保持不变。(还是没懂)
2.1.3.3泛型 Generics
Dafny同其他语言一样都有泛型任何类、方法、函数都可以有类型参数在中申明该数据类型T
class MyMultisetT {/*...*/
} //类泛型
datatype TreeT Leaf | Node(TreeT, T, TreeT) //自定义数据泛型
method FindT(key: T, collection: TreeT) { //方法泛型/*...*/
}function IfThenElseT(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 值。 每个右侧都可以是以下形式之一的表达式或对象创建 new T new T.Init(ExprList) new T(ExprList) new T[SizeExpr] new T[SizeExpr0, SizeExpr1] 第一种形式分配一个类型为 T 的对象。
第二种形式另外在新分配的对象上调用初始化方法或构造函数。
第三种形式是当调用匿名构造函数时的语法。
其他形式分别了T是一维和二维数组对象的匿名构造方法
assert 声明
assert 语句判断后面的表达式结果是否为真由验证器验证。
print 打印语句
打印语句将给定打印表达式的值输出到标准输出。字符串中的字符可以转义例如对 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[m1]、……直到但不包括 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 分支。
三、环境配置及实例
内配置 打开[]文件 插件默认在每次执行文件保存操作后尝试对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
