Dafny

 

关于Dafny的资料

最近在学Dafny,一种可以验证自己的程序语言。本来在rise4fun.com有教学资源,但是现在网站挂了(Waterloo fork了一个网站)在这里囤一下相关的学习材料和笔记。

官方资源

Dafny Documentation

U of Edinburgh 请 KRML 的讲座 介绍了一些历史(尤其是verification的)

Dafny blog 也很不错!

KRML的dafny power user website

课程资料

UNSW SENG2011 by Albert Nymeyer

UNSW 的 Albert Nymeyer 教授每年开设的 Software Engineering Workshop 2A会完整的覆盖Dafny

16年课程网站 Lecture条目下可以访问课程计划 前四节课的slides可以下载

21年课程网站 很多东西访问不了 但是可以访问他的课件 鸡肋的是访问不了course schedule不知道课件的阅读顺序 但是可以通过文件的修改时间来猜测顺序(我可能会列一下自己看的顺序)

这位同学还善良地留下了自己19年的课程笔记

CMU 15-811 by Bryan Parno

CMU研究生课 Verifying Complex Systems

第一个月会从SAT/SMT开始讲 然后后面三次课学Dafny 两个话题都有相关作业

这门课的内容可能更有用一些。

其他混杂的会提及Dafny的课程(还没有好好看)

Formal software Development Methods @ UIUC 课程网站

Principles of Software @ RPI 课程网站

Systems and Formal Methods (Lecture 3) @ Cornell 课程网站

Formal Methods in Software Engineering @ U of Iowa (请了Leino来讲的) 课程网站

Dafny Mini-course @ ICL 课程网站

以色列某学校 貌似有square root的例子

UNSW SENG2011 笔记

各slides阅读顺序及内容

Hoare Logic

Predicate Translation, Hoare Logic 1 & 2

Intro to Dafny

Dafny Intro, Dafny Basics, Initialisation Strength, Validate Verify

Array Quantifiers, Invariant WYSIWYG, Recursion Termination, Function Predicates, Induction DataTypes

(Examples) Search Insertion Sort, Dutchflag Sort

Sets Sequences

Lemma

Proof Power, Lemma Direct Contra, Lemma Induction Levels, Lemma Induction More, Lemma 100 Prisoners (eg)

Complex Structure

Classes, Verifying Data, Verifying Ghost Data

Examples: Object Dynamic Frames, QuickSort

Some Challenges

VerifyThis2016

第一题有dafny答案

VerifyThis2017

所有题都有dafny solution