-
-
Notifications
You must be signed in to change notification settings - Fork 84
/
dafny.scroll
127 lines (111 loc) · 5.38 KB
/
dafny.scroll
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
import ../code/conceptPage.scroll
id dafny
name Dafny
appeared 2009
creators K. Rustan M. Leino
tags pl
website https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/
isOpenSource true
writtenIn csharp markdown java yaml f-sharp toml python go xml html make bash javascript tex bourne-shell gradle css json rust diff svg
tryItOnline dafny
clocExtensions dfy
fileType text
rosettaCode http://www.rosettacode.org/wiki/Category:Dafny
quineRelay Dafny
centralPackageRepositoryCount 0
ubuntuPackage dafny
repoStats
firstCommit 2009
commits 8344
committers 144
files 5636
newestCommit 2024
originCommunity Microsoft
helloWorldCollection Dafny
// Hello world in Dafny
method Main() {
print "Hello, World!\n";
}
rijuRepl https://riju.codes/dafny
example
method Main() {
print "Hello, world!\n";
}
githubRepo https://github.com/Microsoft/dafny
stars 1714
forks 206
subscribers 76
created 2016
updated 2022
firstCommit 2009
description Dafny is a verification-aware programming language
issues 550
lineCommentToken //
printToken print
hasLineComments true
// A comment
hasComments true
// A comment
hasPrintDebugging true
hasSemanticIndentation false
wikipedia https://en.wikipedia.org/wiki/Dafny_(programming_language)
example
datatype List = Nil | Link(data:int,next:List)
function sum(l:List): int {
match l
case Nil => 0
case Link(d,n) => d + sum(n)
}
predicate isNatList(l:List) {
match l
case Nil => true
case Link(d,n) => d >= 0 && isNatList(n)
}
ghost method NatSumLemma(l:List, n:int)
requires isNatList(l) && n == sum(l)
ensures n >= 0
{
match l
case Nil =>
// Discharged Automatically
case Link(data,next) => {
// Apply Inductive Hypothesis
NatSumLemma(next,sum(next));
// Check what known by Dafny
assert data >= 0;
}
}
related csharp spec-sharp spark idris agda
summary Dafny is an imperative compiled language that targets C# and supports formal specification through preconditions, postconditions, loop invariants and loop variants. The language combines ideas primarily from the Functional and Imperative paradigms, and includes limited support for Object-Oriented Programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his previous work on developing ESC/Modula-3, ESC/Java, and Spec#. Dafny is been used widely in teaching and features regularly in software verification competitions (e.g. VSTTE'08, VSCOMP'10, COST'11, and VerifyThis'12). Dafny was designed to provide a simple introduction to formal specification and verification and has been used widely in teaching. Dafny follows in the lineage of many previous tools, including SPARK/Ada, ESC/Java, Spec#, Whiley, Why3 and Frama-C. Such tools rely on the use of automated theorem proving to discharge proof obligations unlike, for example, those based on dependent types (e.g. Idris, Agda) which require more human intervention. Dafny builds on the Boogie intermediate language which uses the Z3 automated theorem prover for discharging proof obligations.
pageId 56073623
created 2018
backlinksCount 4
revisionCount 2
dailyPageViews 1
appeared 2009
githubBigQuery Dafny
repos 1
users 1
isbndb 1
year|publisher|title|authors|isbn13
2022|Apress|Introducing Software Verification with Dafny Language: Proving Program Correctness|Sitnikovski, Boro|9781484279786
githubLanguage Dafny
type programming
fileExtensions dfy
interpreters dafny
aceMode text
tmScope text.dfy.dafny
repos 157
semanticScholar 11
year|title|doi|citations|influentialCitations|authors|paperId
2014|The Dafny Integrated Development Environment|10.4204/EPTCS.149.2|52|2|K. Leino and Valentin Wüstholz|53a027ff333e4eb1d9f76152ce294922f5cbacfd
2012|Developing verified programs with Dafny|10.1145/2402676.2402682|42|5|K. Leino|e294024f911de532d86a69a28b319e6f0bb1aadb
2017|Accessible Software Verification with Dafny|10.1109/MS.2017.4121212|27|1|K. Leino|07fa56cf259459a785328c33115a92071eaf450a
2012|Developing verified programs with Dafny|10.1145/2402676.2402682|9|0|K. Leino|2538a75fca5da05594c6eb3ee6dc6fedd64262df
2016|Tactics for the Dafny Program Verifier|10.1007/978-3-662-49674-9_3|8|0|G. Grov and V. Tumas|c83cffd0168388dd5e6eb8ee32b7ac58ce3ce6be
2015|Automatic verification of Dafny programs with traits|10.1145/2786536.2786542|6|0|Reza Ahmadi and K. Leino and J. Nummenmaa|f635d2bc6f0bec27f421d25e9bcbbf359e997ddb
2017|Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny|10.29007/5zjp|4|0|Sylvia Grewe and Sebastian Erdweg and M. Mezini|7c630bfc43ed8e908b4786b590ec44bd181eae41
2017|A Tutorial on Using Dafny to Construct Verified Software|10.4204/EPTCS.237.1|2|0|P. Lucio|6ccb9ac2ce28800d64389e1a2d947ffae5e75adc
2018|Towards progressive program verification in Dafny|10.1145/3264637.3264649|2|0|Ismael Figueroa and Bruno García and Paul Leger|145b3453b2df6f00fb93275acdef2958235cdc00
2019|An Assertional Proof of Red–Black Trees Using Dafny|10.1007/s10817-019-09534-y|2|0|R. Peña|9b5c59696f3cc11c0f40b071560be0c10ebd6c02
2016|Mechanised Verification Patterns for Dafny|10.1007/978-3-319-48989-6_20|1|0|G. Grov and Yuhui Lin and V. Tumas|6ee1f76da9b91f0d493e28afdfa796a48781fc25